Theorem el1o 8480

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

Syntax hints:   ↔ wb 209   = wceq 1567   ∈ wcel 2149  ∅c0 4294  {csn 4594  1_oc1o 8446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-nul 5271

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-un 3918  df-nul 4295  df-sn 4595  df-suc 6367  df-1o 8453

This theorem is referenced by:  ord1eln01  8481  ord2eln012  8482  0lt1o  8489  oelim2  8581  oeeulem  8587  oaabs2  8635  cantnff  9643  cnfcom3lem  9672  cfsuc  10241  pf1ind  22484  mavmul0  22678  cramer0  22816  selvply1rhmlem2  33856  cantnfresb  43943  omabs2  43951  omcl3g  43953  f1omoOLD  49557  isinito3  50163