Theorem el1o 8508

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ∈ wcel 2144  ∅c0 4277  {csn 4584  1_oc1o 8474

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 4046  df-un 4150  df-nul 4278  df-sn 4585  df-suc 6370  df-1o 8481

This theorem is used by:  ord1eln01  8509  ord2eln012  8510  0lt1o  8517  oelim2  8609  oeeulem  8615  oaabs2  8663  cantnff  9680  cnfcom3lem  9709  cfsuc  10340  pf1ind  22680  mavmul0  22874  cramer0  23015  selvply1rhmlem2  34201  cantnfresb  44433  omabs2  44441  omcl3g  44443  f1omoOLD  50115  isinito3  50742