Theorem el1o 8533

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ∅c0 4333  {csn 4626  1_oc1o 8499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-nul 4334  df-sn 4627  df-suc 6390  df-1o 8506

This theorem is referenced by:  ord1eln01  8534  ord2eln012  8535  0lt1o  8542  oelim2  8633  oeeulem  8639  oaabs2  8687  cantnff  9714  cnfcom3lem  9743  cfsuc  10297  pf1ind  22359  mavmul0  22558  cramer0  22696  cantnfresb  43337  omabs2  43345  omcl3g  43347  f1omo  48792