Theorem el1o 8432

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 8414	. . 3 ⊢ 1o = {∅}
2	1	eleq2i 2829	. 2 ⊢ (𝐴 ∈ 1o ↔ 𝐴 ∈ {∅})
3		0ex 5254	. . 3 ⊢ ∅ ∈ V
4	3	elsn2 4624	. 2 ⊢ (𝐴 ∈ {∅} ↔ 𝐴 = ∅)
5	2, 4	bitri 275	1 ⊢ (𝐴 ∈ 1o ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∅c0 4287  {csn 4582  1_oc1o 8400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5253

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-un 3908  df-nul 4288  df-sn 4583  df-suc 6331  df-1o 8407

This theorem is referenced by:  ord1eln01  8433  ord2eln012  8434  0lt1o  8441  oelim2  8533  oeeulem  8539  oaabs2  8587  cantnff  9595  cnfcom3lem  9624  cfsuc  10179  pf1ind  22311  mavmul0  22508  cramer0  22646  cantnfresb  43681  omabs2  43689  omcl3g  43691  f1omoOLD  49253  isinito3  49859