Theorem el1o 8419

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∅c0 4282  {csn 4577  1_oc1o 8387

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 2705  ax-nul 5248

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-un 3903  df-nul 4283  df-sn 4578  df-suc 6320  df-1o 8394

This theorem is referenced by:  ord1eln01  8420  ord2eln012  8421  0lt1o  8428  oelim2  8519  oeeulem  8525  oaabs2  8573  cantnff  9575  cnfcom3lem  9604  cfsuc  10159  pf1ind  22290  mavmul0  22487  cramer0  22625  cantnfresb  43481  omabs2  43489  omcl3g  43491  f1omoOLD  49055  isinito3  49661