Theorem el1o 8420

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 8402	. . 3 ⊢ 1o = {∅}
2	1	eleq2i 2831	. 2 ⊢ (𝐴 ∈ 1o ↔ 𝐴 ∈ {∅})
3		0ex 5229	. . 3 ⊢ ∅ ∈ V
4	3	elsn2 4597	. 2 ⊢ (𝐴 ∈ {∅} ↔ 𝐴 = ∅)
5	2, 4	bitri 276	1 ⊢ (𝐴 ∈ 1o ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 207   = wceq 1547   ∈ wcel 2119  ∅c0 4261  {csn 4555  1_oc1o 8388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-nul 5228

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886  df-un 3888  df-nul 4262  df-sn 4556  df-suc 6316  df-1o 8395

This theorem is referenced by:  ord1eln01  8421  ord2eln012  8422  0lt1o  8429  oelim2  8521  oeeulem  8527  oaabs2  8575  cantnff  9586  cnfcom3lem  9615  cfsuc  10170  pf1ind  22341  mavmul0  22535  cramer0  22673  selvply1rhmlem2  33705  cantnfresb  43769  omabs2  43777  omcl3g  43779  f1omoOLD  49384  isinito3  49990