Theorem on0eln0 6246

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

Assertion

Ref	Expression
on0eln0	⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))

Proof of Theorem on0eln0

Step	Hyp	Ref	Expression
1		eloni 6201	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ord0eln0 6245	. 2 ⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
3	1, 2	syl 17	1 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2114   ≠ wne 3016  ∅c0 4291  Ord word 6190  Oncon0 6191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-tr 5173  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-ord 6194  df-on 6195

This theorem is referenced by:  ondif1  8126  oe0lem  8138  oevn0  8140  oa00  8185  omord  8194  om00  8201  om00el  8202  omeulem1  8208  omeulem2  8209  oewordri  8218  oeordsuc  8220  oelim2  8221  oeoa  8223  oeoe  8225  oeeui  8228  omabs  8274  omxpenlem  8618  cantnff  9137  cantnfp1  9144  cantnflem1d  9151  cantnflem1  9152  cantnflem3  9154  cantnflem4  9155  cantnf  9156  cnfcomlem  9162  cnfcom3  9167  r1tskina  10204  onsucconni  33785  onint1  33797  frlmpwfi  39718