Theorem on0eln0 6425

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2146   ≠ wne 2961  ∅c0 4289  Ord word 6366  Oncon0 6367

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

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 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-tr 5224  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-ord 6370  df-on 6371

This theorem is used by:  ondif1  8495  oe0lem  8507  oevn0  8509  oa00  8553  omord  8562  om00  8569  om00el  8570  omeulem1  8576  omeulem2  8577  oewordri  8587  oeordsuc  8589  oelim2  8590  oeoa  8592  oeoe  8594  oeeui  8597  omabs  8646  omxpenlem  9076  cantnff  9653  cantnfp1  9660  cantnflem1d  9667  cantnflem1  9668  cantnflem3  9670  cantnflem4  9671  cantnf  9672  cnfcomlem  9678  cnfcom3  9683  r1tskina  10785  onsucconni  36989  onint1  37001  frlmpwfi  43866  omge1  44065  omge2  44066  omlim2  44067  omord2lim  44068  omord2i  44069  dflim5  44097  tfsconcatb0  44112  tfsconcat0b  44114  oaun3lem1  44142  naddwordnexlem4  44169  omltoe  44174