Theorem el1o 8458

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 8438	. . 3 ⊢ 1o = {∅}
2	1	eleq2i 2853	. 2 ⊢ (𝐴 ∈ 1o ↔ 𝐴 ∈ {∅})
3		0ex 5254	. . 3 ⊢ ∅ ∈ V
4	3	elsn2 4621	. 2 ⊢ (𝐴 ∈ {∅} ↔ 𝐴 = ∅)
5	2, 4	bitri 277	1 ⊢ (𝐴 ∈ 1o ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 208   = wceq 1559   ∈ wcel 2141  ∅c0 4283  {csn 4579  1_oc1o 8424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5253

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-dif 3905  df-un 3907  df-nul 4284  df-sn 4580  df-suc 6347  df-1o 8431

This theorem is referenced by:  ord1eln01  8459  ord2eln012  8460  0lt1o  8467  oelim2  8559  oeeulem  8565  oaabs2  8613  cantnff  9623  cnfcom3lem  9652  cfsuc  10208  pf1ind  22406  mavmul0  22600  cramer0  22738  selvply1rhmlem2  33779  cantnfresb  43862  omabs2  43870  omcl3g  43872  f1omoOLD  49476  isinito3  50082