Theorem el1o 8459

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∅c0 4296  {csn 4589  1_oc1o 8427

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 5261

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 3449  df-dif 3917  df-un 3919  df-nul 4297  df-sn 4590  df-suc 6338  df-1o 8434

This theorem is referenced by:  ord1eln01  8460  ord2eln012  8461  0lt1o  8468  oelim2  8559  oeeulem  8565  oaabs2  8613  cantnff  9627  cnfcom3lem  9656  cfsuc  10210  pf1ind  22242  mavmul0  22439  cramer0  22577  cantnfresb  43313  omabs2  43321  omcl3g  43323  f1omoOLD  48882  isinito3  49489