Theorem el1o 8430

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∅c0 4273  {csn 4567  1_oc1o 8398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-un 3894  df-nul 4274  df-sn 4568  df-suc 6329  df-1o 8405

This theorem is referenced by:  ord1eln01  8431  ord2eln012  8432  0lt1o  8439  oelim2  8531  oeeulem  8537  oaabs2  8585  cantnff  9595  cnfcom3lem  9624  cfsuc  10179  pf1ind  22320  mavmul0  22517  cramer0  22655  cantnfresb  43752  omabs2  43760  omcl3g  43762  f1omoOLD  49369  isinito3  49975