Theorem on0eln0 5464

Description: An ordinal number contains zero iff it is nonzero. (Contributed by NM, 6-Dec-2004.)

Assertion

Ref	Expression
on0eln0	|- ( A e. On -> ( (/) e. A <-> A =/= (/) ) )

Proof of Theorem on0eln0

Step	Hyp	Ref	Expression
1		eloni 5419	. 2 |- ( A e. On -> Ord A )
2		ord0eln0 5463	. 2 |- ( Ord A -> ( (/) e. A <-> A =/= (/) ) )
3	1, 2	syl 17	1 |- ( A e. On -> ( (/) e. A <-> A =/= (/) ) )

Syntax hints:   -> wi 4   <-> wb 184   e. wcel 1842   =/= wne 2598   (/)c0 3737   Ord word 5408   Oncon0 5409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-sbc 3277  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-opab 4453  df-tr 4489  df-eprel 4733  df-po 4743  df-so 4744  df-fr 4781  df-we 4783  df-ord 5412  df-on 5413

This theorem is referenced by:  ondif1  7187  oe0lem  7199  oevn0  7201  oa00  7244  omord  7253  om00  7260  om00el  7261  omeulem1  7267  omeulem2  7268  oewordri  7277  oeordsuc  7279  oelim2  7280  oeoa  7282  oeoe  7284  oeeui  7287  omabs  7332  omxpenlem  7655  cantnff  8124  cantnfp1lem2  8129  cantnfp1lem3  8130  cantnfp1  8131  cantnflem1d  8138  cantnflem1  8139  cantnflem3  8141  cantnflem4  8142  cantnf  8143  cantnfp1lem2OLD  8155  cantnfp1lem3OLD  8156  cantnfp1OLD  8157  cantnflem1dOLD  8161  cantnflem1OLD  8162  cantnflem3OLD  8163  cantnflem4OLD  8164  cantnfOLD  8165  cnfcomlem  8174  cnfcom3  8179  cnfcomlemOLD  8182  cnfcom3OLD  8187  r1tskina  9189  onsucconi  30656  onint1  30668  frlmpwfi  35390