Theorem on0eln0 4939

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 4894	. 2 |- ( A e. On -> Ord A )
2		ord0eln0 4938	. 2 |- ( Ord A -> ( (/) e. A <-> A =/= (/) ) )
3	1, 2	syl 16	1 |- ( A e. On -> ( (/) e. A <-> A =/= (/) ) )

Syntax hints:   -> wi 4   <-> wb 184   e. wcel 1767   =/= wne 2662   (/)c0 3790   Ord word 4883   Oncon0 4884

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-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pr 4692

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-tr 4547  df-eprel 4797  df-po 4806  df-so 4807  df-fr 4844  df-we 4846  df-ord 4887  df-on 4888

This theorem is referenced by:  ondif1  7163  oe0lem  7175  oevn0  7177  oa00  7220  omord  7229  om00  7236  om00el  7237  omeulem1  7243  omeulem2  7244  oewordri  7253  oeordsuc  7255  oelim2  7256  oeoa  7258  oeoe  7260  oeeui  7263  omabs  7308  omxpenlem  7630  cantnff  8105  cantnfp1lem2  8110  cantnfp1lem3  8111  cantnfp1  8112  cantnflem1d  8119  cantnflem1  8120  cantnflem3  8122  cantnflem4  8123  cantnf  8124  cantnfp1lem2OLD  8136  cantnfp1lem3OLD  8137  cantnfp1OLD  8138  cantnflem1dOLD  8142  cantnflem1OLD  8143  cantnflem3OLD  8144  cantnflem4OLD  8145  cantnfOLD  8146  cnfcomlem  8155  cnfcom3  8160  cnfcomlemOLD  8163  cnfcom3OLD  8168  r1tskina  9172  onsucconi  29836  onint1  29848  frlmpwfi  30980