Theorem el1o 8422

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∅c0 4285  {csn 4580  1_oc1o 8390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-un 3906  df-nul 4286  df-sn 4581  df-suc 6323  df-1o 8397

This theorem is referenced by:  ord1eln01  8423  ord2eln012  8424  0lt1o  8431  oelim2  8523  oeeulem  8529  oaabs2  8577  cantnff  9583  cnfcom3lem  9612  cfsuc  10167  pf1ind  22299  mavmul0  22496  cramer0  22634  cantnfresb  43566  omabs2  43574  omcl3g  43576  f1omoOLD  49139  isinito3  49745