{
  "citations" : [ {
    "textCitation" : "[See cncnpi on Metamath](http://us.metamath.org/mpegif/cncnpi.html)"
  } ],
  "names" : [ "cncnpi" ],
  "language" : "METAMATH_SET_MM",
  "lookupTerms" : [ "#T_cX", "#T_wceq", "#T_cuni", "#T_cJ", "#T_cF", "#T_wcel", "#T_cJ", "#T_ccn", "#T_cK", "#T_wa", "#T_cA", "#T_wcel", "#T_cX", "#T_wi", "#T_cF", "#T_wcel", "#T_cJ", "#T_ccnp", "#T_cK", "#T_cfv", "#T_cA" ],
  "metaLanguage" : "METAMATH",
  "remarks" : " A continuous function is continuous at all points.  One direction of Theorem 7.2(g) of [Munkres] p. 107.  (Contributed by <NAME>, 20-Nov-2006.)  (Proof shortened by <NAME>, 21-Aug-2015.) ",
  "statement" : "cnsscnp.1 $e |- X = U. J $.\ncncnpi $p |- ( ( F e. ( J Cn K ) /\\ A e. X ) -> F e. ( ( J CnP K ) ` A ) ) $."
}