Theorem on0eln0 6419

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2145   ≠ wne 2957  ∅c0 4282  Ord word 6360  Oncon0 6361

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-tr 5217  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6364  df-on 6365

This theorem is used by:  ondif1  8492  oe0lem  8504  oevn0  8506  oa00  8550  omord  8559  om00  8566  om00el  8567  omeulem1  8573  omeulem2  8574  oewordri  8584  oeordsuc  8586  oelim2  8587  oeoa  8589  oeoe  8591  oeeui  8594  omabs  8643  omxpenlem  9080  cantnff  9657  cantnfp1  9664  cantnflem1d  9671  cantnflem1  9672  cantnflem3  9674  cantnflem4  9675  cantnf  9676  cnfcomlem  9682  cnfcom3  9687  r1tskina  10795  onsucconni  37064  onint1  37076  frlmpwfi  43947  omge1  44146  omge2  44147  omlim2  44148  omord2lim  44149  omord2i  44150  dflim5  44178  tfsconcatb0  44193  tfsconcat0b  44195  oaun3lem1  44223  naddwordnexlem4  44250  omltoe  44255