Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  1stcclb Unicode version

Theorem 1stcclb 17186
 Description: A property of points in a first-countable topology. (Contributed by Jeff Hankins, 22-Aug-2009.)
Hypothesis
Ref Expression
1stcclb.1
Assertion
Ref Expression
1stcclb
Distinct variable groups:   ,,,   ,,,   ,,,

Proof of Theorem 1stcclb
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 1stcclb.1 . . . 4
21is1stc2 17184 . . 3
32simprbi 450 . 2
4 eleq1 2356 . . . . . . 7
5 eleq1 2356 . . . . . . . . 9
65anbi1d 685 . . . . . . . 8
76rexbidv 2577 . . . . . . 7
84, 7imbi12d 311 . . . . . 6
98ralbidv 2576 . . . . 5
109anbi2d 684 . . . 4
1110rexbidv 2577 . . 3
1211rspcv 2893 . 2
133, 12mpan9 455 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 358   wceq 1632   wcel 1696  wral 2556  wrex 2557   wss 3165  cpw 3638  cuni 3843   class class class wbr 4039  com 4672   cdom 6877  ctop 16647  c1stc 17179 This theorem is referenced by:  1stcfb  17187  1stcrest  17195  lly1stc  17238  tx1stc  17360 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-in 3172  df-ss 3179  df-pw 3640  df-uni 3844  df-1stc 17181
 Copyright terms: Public domain W3C validator