Theorem on0eln0 6409

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108   ≠ wne 2932  ∅c0 4308  Ord word 6351  Oncon0 6352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-tr 5230  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-ord 6355  df-on 6356

This theorem is referenced by:  ondif1  8513  oe0lem  8525  oevn0  8527  oa00  8571  omord  8580  om00  8587  om00el  8588  omeulem1  8594  omeulem2  8595  oewordri  8604  oeordsuc  8606  oelim2  8607  oeoa  8609  oeoe  8611  oeeui  8614  omabs  8663  omxpenlem  9087  cantnff  9688  cantnfp1  9695  cantnflem1d  9702  cantnflem1  9703  cantnflem3  9705  cantnflem4  9706  cantnf  9707  cnfcomlem  9713  cnfcom3  9718  r1tskina  10796  onsucconni  36455  onint1  36467  frlmpwfi  43122  omge1  43321  omge2  43322  omlim2  43323  omord2lim  43324  omord2i  43325  dflim5  43353  tfsconcatb0  43368  tfsconcat0b  43370  oaun3lem1  43398  naddwordnexlem4  43425  omltoe  43431