Theorem on0eln0 6442

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2106   ≠ wne 2938  ∅c0 4339  Ord word 6385  Oncon0 6386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-ord 6389  df-on 6390

This theorem is referenced by:  ondif1  8538  oe0lem  8550  oevn0  8552  oa00  8596  omord  8605  om00  8612  om00el  8613  omeulem1  8619  omeulem2  8620  oewordri  8629  oeordsuc  8631  oelim2  8632  oeoa  8634  oeoe  8636  oeeui  8639  omabs  8688  omxpenlem  9112  cantnff  9712  cantnfp1  9719  cantnflem1d  9726  cantnflem1  9727  cantnflem3  9729  cantnflem4  9730  cantnf  9731  cnfcomlem  9737  cnfcom3  9742  r1tskina  10820  onsucconni  36420  onint1  36432  frlmpwfi  43087  omge1  43287  omge2  43288  omlim2  43289  omord2lim  43290  omord2i  43291  dflim5  43319  tfsconcatb0  43334  tfsconcat0b  43336  oaun3lem1  43364  naddwordnexlem4  43391  omltoe  43397