Theorem on0eln0 6441

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2147   ≠ wne 2959  ∅c0 4281  Ord word 6382  Oncon0 6383

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-tr 5217  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-ord 6386  df-on 6387

This theorem is used by:  ondif1  8540  oe0lem  8552  oevn0  8554  oa00  8598  omord  8607  om00  8614  om00el  8615  omeulem1  8621  omeulem2  8622  oewordri  8632  oeordsuc  8634  oelim2  8635  oeoa  8637  oeoe  8639  oeeui  8642  omabs  8691  omxpenlem  9128  cantnff  9705  cantnfp1  9712  cantnflem1d  9719  cantnflem1  9720  cantnflem3  9722  cantnflem4  9723  cantnf  9724  cnfcomlem  9730  cnfcom3  9735  r1tskina  10897  maxssj0  36019  k39o  36030  j0le  36032  k3n0j0lt  36033  fnlfvk3n0  36041  onsucconni  37416  onint1  37428  frlmpwfi  44304  omge1  44502  omge2  44503  omlim2  44504  omord2lim  44505  omord2i  44506  dflim5  44534  tfsconcatb0  44549  tfsconcat0b  44551  oaun3lem1  44579  naddwordnexlem4  44606  omltoe  44611