Theorem on0eln0 6413

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2145   ≠ wne 2956  ∅c0 4279  Ord word 6354  Oncon0 6355

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 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6358  df-on 6359

This theorem is used by:  ondif1  8493  oe0lem  8505  oevn0  8507  oa00  8551  omord  8560  om00  8567  om00el  8568  omeulem1  8574  omeulem2  8575  oewordri  8585  oeordsuc  8587  oelim2  8588  oeoa  8590  oeoe  8592  oeeui  8595  omabs  8644  omxpenlem  9081  cantnff  9659  cantnfp1  9666  cantnflem1d  9673  cantnflem1  9674  cantnflem3  9676  cantnflem4  9677  cantnf  9678  cnfcomlem  9684  cnfcom3  9689  r1tskina  10848  onsucconni  37195  onint1  37207  frlmpwfi  44058  omge1  44257  omge2  44258  omlim2  44259  omord2lim  44260  omord2i  44261  dflim5  44289  tfsconcatb0  44304  tfsconcat0b  44306  oaun3lem1  44334  naddwordnexlem4  44361  omltoe  44366