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

Theorem is1stc2 17506
 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 17505 . 2
3 elin 3531 . . . . . . . . . . . . 13
4 vex 2960 . . . . . . . . . . . . . . 15
54elpw 3806 . . . . . . . . . . . . . 14
65anbi2i 677 . . . . . . . . . . . . 13
73, 6bitri 242 . . . . . . . . . . . 12
87anbi2i 677 . . . . . . . . . . 11
9 an12 774 . . . . . . . . . . 11
108, 9bitri 242 . . . . . . . . . 10
1110exbii 1593 . . . . . . . . 9
12 eluni 4019 . . . . . . . . 9
13 df-rex 2712 . . . . . . . . 9
1411, 12, 133bitr4i 270 . . . . . . . 8
1514imbi2i 305 . . . . . . 7
1615ralbii 2730 . . . . . 6
1716anbi2i 677 . . . . 5
1817rexbii 2731 . . . 4
1918ralbii 2730 . . 3
2019anbi2i 677 . 2
212, 20bitri 242 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360  wex 1551   wceq 1653   wcel 1726  wral 2706  wrex 2707   cin 3320   wss 3321  cpw 3800  cuni 4016   class class class wbr 4213  com 4846   cdom 7108  ctop 16959  c1stc 17501 This theorem is referenced by:  1stcclb  17508  2ndc1stc  17515  1stcrest  17517  lly1stc  17560  tx1stc  17683  met1stc  18552 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ral 2711  df-rex 2712  df-rab 2715  df-v 2959  df-in 3328  df-ss 3335  df-pw 3802  df-uni 4017  df-1stc 17503
 Copyright terms: Public domain W3C validator