Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pconcn Structured version   Unicode version

Theorem pconcn 29397
 Description: The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.)
Hypothesis
Ref Expression
ispcon.1
Assertion
Ref Expression
pconcn PCon
Distinct variable groups:   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem pconcn
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ispcon.1 . . . . 5
21ispcon 29396 . . . 4 PCon
32simprbi 462 . . 3 PCon
4 eqeq2 2415 . . . . . 6
54anbi1d 703 . . . . 5
65rexbidv 2915 . . . 4
7 eqeq2 2415 . . . . . 6
87anbi2d 702 . . . . 5
98rexbidv 2915 . . . 4
106, 9rspc2v 3166 . . 3
113, 10syl5com 28 . 2 PCon
12113impib 1193 1 PCon
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 367   w3a 972   wceq 1403   wcel 1840  wral 2751  wrex 2752  cuni 4188  cfv 5523  (class class class)co 6232  cc0 9440  c1 9441  ctop 19576   ccn 19908  cii 21561  PConcpcon 29392 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378 This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 974  df-tru 1406  df-ex 1632  df-nf 1636  df-sb 1762  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-ral 2756  df-rex 2757  df-rab 2760  df-v 3058  df-dif 3414  df-un 3416  df-in 3418  df-ss 3425  df-nul 3736  df-if 3883  df-sn 3970  df-pr 3972  df-op 3976  df-uni 4189  df-br 4393  df-iota 5487  df-fv 5531  df-ov 6235  df-pcon 29394 This theorem is referenced by:  cnpcon  29403  pconcon  29404  txpcon  29405  ptpcon  29406  conpcon  29408  pconpi1  29410  cvmlift3lem2  29493  cvmlift3lem7  29498
 Copyright terms: Public domain W3C validator