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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2104   ≠ wne 2938  ∅c0 4321  Ord word 6362  Oncon0 6363

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-ord 6366  df-on 6367

This theorem is referenced by:  ondif1  8503  oe0lem  8515  oevn0  8517  oa00  8561  omord  8570  om00  8577  om00el  8578  omeulem1  8584  omeulem2  8585  oewordri  8594  oeordsuc  8596  oelim2  8597  oeoa  8599  oeoe  8601  oeeui  8604  omabs  8652  omxpenlem  9075  cantnff  9671  cantnfp1  9678  cantnflem1d  9685  cantnflem1  9686  cantnflem3  9688  cantnflem4  9689  cantnf  9690  cnfcomlem  9696  cnfcom3  9701  r1tskina  10779  onsucconni  35625  onint1  35637  frlmpwfi  42142  omge1  42349  omge2  42350  omlim2  42351  omord2lim  42352  omord2i  42353  dflim5  42381  tfsconcatb0  42396  tfsconcat0b  42398  oaun3lem1  42426  naddwordnexlem4  42454  omltoe  42460