Theorem on0eln0 6392

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109   ≠ wne 2926  ∅c0 4299  Ord word 6334  Oncon0 6335

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339

This theorem is referenced by:  ondif1  8468  oe0lem  8480  oevn0  8482  oa00  8526  omord  8535  om00  8542  om00el  8543  omeulem1  8549  omeulem2  8550  oewordri  8559  oeordsuc  8561  oelim2  8562  oeoa  8564  oeoe  8566  oeeui  8569  omabs  8618  omxpenlem  9047  cantnff  9634  cantnfp1  9641  cantnflem1d  9648  cantnflem1  9649  cantnflem3  9651  cantnflem4  9652  cantnf  9653  cnfcomlem  9659  cnfcom3  9664  r1tskina  10742  onsucconni  36432  onint1  36444  frlmpwfi  43094  omge1  43293  omge2  43294  omlim2  43295  omord2lim  43296  omord2i  43297  dflim5  43325  tfsconcatb0  43340  tfsconcat0b  43342  oaun3lem1  43370  naddwordnexlem4  43397  omltoe  43403