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

Theorem 1stctop 17537
 Description: A first-countable topology is a topology. (Contributed by Jeff Hankins, 22-Aug-2009.)
Assertion
Ref Expression
1stctop

Proof of Theorem 1stctop
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2442 . . 3
21is1stc 17535 . 2
32simplbi 448 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 360   wcel 1727  wral 2711  wrex 2712   cin 3305  cpw 3823  cuni 4039   class class class wbr 4237  com 4874   cdom 7136  ctop 16989  c1stc 17531 This theorem is referenced by:  1stcfb  17539  1stcrest  17547  1stcelcls  17555  lly1stc  17590  1stckgen  17617  tx1stc  17713 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423 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 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ral 2716  df-rex 2717  df-rab 2720  df-v 2964  df-in 3313  df-ss 3320  df-pw 3825  df-uni 4040  df-1stc 17533
 Copyright terms: Public domain W3C validator