Theorem on0eln0 4793

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 4748	. 2 |- ( A e. On -> Ord A )
2		ord0eln0 4792	. 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 1756   =/= wne 2620   (/)c0 3656   Ord word 4737   Oncon0 4738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4432  ax-nul 4440  ax-pr 4550

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2739  df-rex 2740  df-rab 2743  df-v 2993  df-sbc 3206  df-dif 3350  df-un 3352  df-in 3354  df-ss 3361  df-pss 3363  df-nul 3657  df-if 3811  df-pw 3881  df-sn 3897  df-pr 3899  df-op 3903  df-uni 4111  df-br 4312  df-opab 4370  df-tr 4405  df-eprel 4651  df-po 4660  df-so 4661  df-fr 4698  df-we 4700  df-ord 4741  df-on 4742

This theorem is referenced by:  ondif1  6960  oe0lem  6972  oevn0  6974  oa00  7017  omord  7026  om00  7033  om00el  7034  omeulem1  7040  omeulem2  7041  oewordri  7050  oeordsuc  7052  oelim2  7053  oeoa  7055  oeoe  7057  oeeui  7060  omabs  7105  omxpenlem  7431  cantnff  7901  cantnfp1lem2  7906  cantnfp1lem3  7907  cantnfp1  7908  cantnflem1d  7915  cantnflem1  7916  cantnflem3  7918  cantnflem4  7919  cantnf  7920  cantnfp1lem2OLD  7932  cantnfp1lem3OLD  7933  cantnfp1OLD  7934  cantnflem1dOLD  7938  cantnflem1OLD  7939  cantnflem3OLD  7940  cantnflem4OLD  7941  cantnfOLD  7942  cnfcomlem  7951  cnfcom3  7956  cnfcomlemOLD  7959  cnfcom3OLD  7964  r1tskina  8968  onsucconi  28302  onint1  28314  frlmpwfi  29476