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

Theorem 1stcclb 19790
 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 19788 . . 3
32simprbi 464 . 2
4 eleq1 2539 . . . . . . 7
5 eleq1 2539 . . . . . . . . 9
65anbi1d 704 . . . . . . . 8
76rexbidv 2978 . . . . . . 7
84, 7imbi12d 320 . . . . . 6
98ralbidv 2906 . . . . 5
109anbi2d 703 . . . 4
1110rexbidv 2978 . . 3
1211rspcv 3215 . 2
133, 12mpan9 469 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wceq 1379   wcel 1767  wral 2817  wrex 2818   wss 3481  cpw 4015  cuni 4250   class class class wbr 4452  com 6694   cdom 7524  ctop 19240  c1stc 19783 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-in 3488  df-ss 3495  df-pw 4017  df-uni 4251  df-1stc 19785 This theorem is referenced by:  1stcfb  19791  1stcrest  19799  lly1stc  19842  tx1stc  19996
 Copyright terms: Public domain W3C validator