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

Theorem is2ndc 19710
 Description: The property of being second-countable. (Contributed by Jeff Hankins, 17-Jan-2010.) (Revised by Mario Carneiro, 21-Mar-2015.)
Assertion
Ref Expression
is2ndc
Distinct variable group:   ,

Proof of Theorem is2ndc
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-2ndc 19704 . . 3
21eleq2i 2545 . 2
3 simpr 461 . . . . 5
4 fvex 5874 . . . . 5
53, 4syl6eqelr 2564 . . . 4
65rexlimivw 2952 . . 3
7 eqeq2 2482 . . . . 5
87anbi2d 703 . . . 4
98rexbidv 2973 . . 3
106, 9elab3 3257 . 2
112, 10bitri 249 1
 Colors of variables: wff setvar class Syntax hints:   wb 184   wa 369   wceq 1379   wcel 1767  cab 2452  wrex 2815  cvv 3113   class class class wbr 4447  cfv 5586  com 6678   cdom 7511  ctg 14686  ctb 19162  c2ndc 19702 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  ax-nul 4576 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-sn 4028  df-pr 4030  df-uni 4246  df-iota 5549  df-fv 5594  df-2ndc 19704 This theorem is referenced by:  2ndctop  19711  2ndci  19712  2ndcsb  19713  2ndcredom  19714  2ndc1stc  19715  2ndcrest  19718  2ndcctbss  19719  2ndcdisj  19720  2ndcomap  19722  2ndcsep  19723  dis2ndc  19724  tx2ndc  19884
 Copyright terms: Public domain W3C validator