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

Theorem is1stc2 17458
 Description: An equivalent way of saying "is a first-countable topology." (Contributed by Jeff Hankins, 22-Aug-2009.) (Revised by Mario Carneiro, 21-Mar-2015.)
Hypothesis
Ref Expression
is1stc.1
Assertion
Ref Expression
is1stc2
Distinct variable groups:   ,,,   ,,,   ,
Allowed substitution hints:   ()   (,,)

Proof of Theorem is1stc2
StepHypRef Expression
1 is1stc.1 . . 3
21is1stc 17457 . 2
3 elin 3490 . . . . . . . . . . . . 13
4 vex 2919 . . . . . . . . . . . . . . 15
54elpw 3765 . . . . . . . . . . . . . 14
65anbi2i 676 . . . . . . . . . . . . 13
73, 6bitri 241 . . . . . . . . . . . 12
87anbi2i 676 . . . . . . . . . . 11
9 an12 773 . . . . . . . . . . 11
108, 9bitri 241 . . . . . . . . . 10
1110exbii 1589 . . . . . . . . 9
12 eluni 3978 . . . . . . . . 9
13 df-rex 2672 . . . . . . . . 9
1411, 12, 133bitr4i 269 . . . . . . . 8
1514imbi2i 304 . . . . . . 7
1615ralbii 2690 . . . . . 6
1716anbi2i 676 . . . . 5
1817rexbii 2691 . . . 4
1918ralbii 2690 . . 3
2019anbi2i 676 . 2
212, 20bitri 241 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359  wex 1547   wceq 1649   wcel 1721  wral 2666  wrex 2667   cin 3279   wss 3280  cpw 3759  cuni 3975   class class class wbr 4172  com 4804   cdom 7066  ctop 16913  c1stc 17453 This theorem is referenced by:  1stcclb  17460  2ndc1stc  17467  1stcrest  17469  lly1stc  17512  tx1stc  17635  met1stc  18504 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385 This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-in 3287  df-ss 3294  df-pw 3761  df-uni 3976  df-1stc 17455
 Copyright terms: Public domain W3C validator