Theorem el1o 8423

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∅c0 4274  {csn 4568  1_oc1o 8391

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 5241

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 3432  df-dif 3893  df-un 3895  df-nul 4275  df-sn 4569  df-suc 6323  df-1o 8398

This theorem is referenced by:  ord1eln01  8424  ord2eln012  8425  0lt1o  8432  oelim2  8524  oeeulem  8530  oaabs2  8578  cantnff  9586  cnfcom3lem  9615  cfsuc  10170  pf1ind  22330  mavmul0  22527  cramer0  22665  cantnfresb  43770  omabs2  43778  omcl3g  43780  f1omoOLD  49381  isinito3  49987