Theorem on0eln0 6399

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 6352	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ord0eln0 6398	. 2 ⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
3	1, 2	syl 17	1 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2141   ≠ wne 2956  ∅c0 4285  Ord word 6341  Oncon0 6342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-tr 5207  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-ord 6345  df-on 6346

This theorem is referenced by:  ondif1  8465  oe0lem  8477  oevn0  8479  oa00  8523  omord  8532  om00  8539  om00el  8540  omeulem1  8546  omeulem2  8547  oewordri  8557  oeordsuc  8559  oelim2  8560  oeoa  8562  oeoe  8564  oeeui  8567  omabs  8616  omxpenlem  9046  cantnff  9626  cantnfp1  9633  cantnflem1d  9640  cantnflem1  9641  cantnflem3  9643  cantnflem4  9644  cantnf  9645  cnfcomlem  9651  cnfcom3  9656  r1tskina  10737  onsucconni  36761  onint1  36773  frlmpwfi  43639  omge1  43838  omge2  43839  omlim2  43840  omord2lim  43841  omord2i  43842  dflim5  43870  tfsconcatb0  43885  tfsconcat0b  43887  oaun3lem1  43915  naddwordnexlem4  43942  omltoe  43947