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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2146  ∅c0 4286  {csn 4591  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 2148  ax-9 2156  ax-ext 2737  ax-nul 5271

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-un 3911  df-nul 4287  df-sn 4592  df-suc 6370  df-1o 8455

This theorem is used by:  ord1eln01  8483  ord2eln012  8484  0lt1o  8491  oelim2  8583  oeeulem  8589  oaabs2  8637  cantnff  9646  cnfcom3lem  9675  cfsuc  10252  pf1ind  22545  mavmul0  22739  cramer0  22877  selvply1rhmlem2  33951  cantnfresb  44084  omabs2  44092  omcl3g  44094  f1omoOLD  49705  isinito3  50311