Theorem el1o 8482

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 8462	. . 3 ⊢ 1o = {∅}
2	1	eleq2i 2852	. 2 ⊢ (𝐴 ∈ 1o ↔ 𝐴 ∈ {∅})
3		0ex 5264	. . 3 ⊢ ∅ ∈ V
4	3	elsn2 4626	. 2 ⊢ (𝐴 ∈ {∅} ↔ 𝐴 = ∅)
5	2, 4	bitri 278	1 ⊢ (𝐴 ∈ 1o ↔ 𝐴 = ∅)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∅c0 4279  {csn 4584  1_oc1o 8448

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-un 3904  df-nul 4280  df-sn 4585  df-suc 6363  df-1o 8455

This theorem is used by:  ord1eln01  8483  ord2eln012  8484  0lt1o  8491  oelim2  8583  oeeulem  8589  oaabs2  8637  cantnff  9653  cnfcom3lem  9682  cfsuc  10259  pf1ind  22580  mavmul0  22774  cramer0  22915  selvply1rhmlem2  34031  cantnfresb  44165  omabs2  44173  omcl3g  44175  f1omoOLD  49820  isinito3  50426