Theorem el1o 8551

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

Syntax hints:   ↔ wb 206   = wceq 1537   ∈ wcel 2108  ∅c0 4352  {csn 4648  1_oc1o 8515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-un 3981  df-nul 4353  df-sn 4649  df-suc 6401  df-1o 8522

This theorem is referenced by:  ord1eln01  8552  ord2eln012  8553  0lt1o  8560  oelim2  8651  oeeulem  8657  oaabs2  8705  cantnff  9743  cnfcom3lem  9772  cfsuc  10326  pf1ind  22380  mavmul0  22579  cramer0  22717  cantnfresb  43286  omabs2  43294  omcl3g  43296  f1omo  48574