Theorem el1o 8496

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∅c0 4279  {csn 4584  1_oc1o 8462

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-un 3904  df-nul 4280  df-sn 4585  df-suc 6367  df-1o 8469

This theorem is used by:  ord1eln01  8497  ord2eln012  8498  0lt1o  8505  oelim2  8597  oeeulem  8603  oaabs2  8651  cantnff  9668  cnfcom3lem  9697  cfsuc  10328  pf1ind  22666  mavmul0  22860  cramer0  23001  selvply1rhmlem2  34146  cantnfresb  44310  omabs2  44318  omcl3g  44320  f1omoOLD  49971  isinito3  50577