Theorem el1o 8494

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

Syntax hints:   ↔ wb 205   = wceq 1541   ∈ wcel 2106  ∅c0 4322  {csn 4628  1_oc1o 8458

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3951  df-un 3953  df-nul 4323  df-sn 4629  df-suc 6370  df-1o 8465

This theorem is referenced by:  ord1eln01  8495  ord2eln012  8496  0lt1o  8503  oelim2  8594  oeeulem  8600  oaabs2  8647  cantnff  9668  cnfcom3lem  9697  cfsuc  10251  pf1ind  21873  mavmul0  22053  cramer0  22191  cantnfresb  42064  omabs2  42072  omcl3g  42074  f1omo  47517