Theorem el1o 8476

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

Syntax hints:   ↔ wb 209   = wceq 1570   ∈ wcel 2143  ∅c0 4286  {csn 4589  1_oc1o 8442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5269

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-un 3910  df-nul 4287  df-sn 4590  df-suc 6366  df-1o 8449

This theorem is referenced by:  ord1eln01  8477  ord2eln012  8478  0lt1o  8485  oelim2  8577  oeeulem  8583  oaabs2  8631  cantnff  9639  cnfcom3lem  9668  cfsuc  10236  pf1ind  22515  mavmul0  22709  cramer0  22847  selvply1rhmlem2  33911  cantnfresb  44051  omabs2  44059  omcl3g  44061  f1omoOLD  49672  isinito3  50278