Theorem el1o 8436

Description: Membership in ordinal one. (Contributed by NM, 5-Jan-2005.)

Assertion

Ref	Expression
el1o	⊢ (𝐴 ∈ 1o ↔ 𝐴 = ∅)

Proof of Theorem el1o

Step	Hyp	Ref	Expression
1		df1o2 8418	. . 3 ⊢ 1o = {∅}
2	1	eleq2i 2820	. 2 ⊢ (𝐴 ∈ 1o ↔ 𝐴 ∈ {∅})
3		0ex 5257	. . 3 ⊢ ∅ ∈ V
4	3	elsn2 4625	. 2 ⊢ (𝐴 ∈ {∅} ↔ 𝐴 = ∅)
5	2, 4	bitri 275	1 ⊢ (𝐴 ∈ 1o ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∅c0 4292  {csn 4585  1_oc1o 8404

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5256

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914  df-un 3916  df-nul 4293  df-sn 4586  df-suc 6326  df-1o 8411

This theorem is referenced by:  ord1eln01  8437  ord2eln012  8438  0lt1o  8445  oelim2  8536  oeeulem  8542  oaabs2  8590  cantnff  9603  cnfcom3lem  9632  cfsuc  10186  pf1ind  22218  mavmul0  22415  cramer0  22553  cantnfresb  43286  omabs2  43294  omcl3g  43296  f1omoOLD  48855  isinito3  49462