Theorem el1o 8490

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

Syntax hints:   ↔ wb 205   = wceq 1533   ∈ wcel 2098  ∅c0 4314  {csn 4620  1_oc1o 8454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-nul 5296

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-dif 3943  df-un 3945  df-nul 4315  df-sn 4621  df-suc 6360  df-1o 8461

This theorem is referenced by:  ord1eln01  8491  ord2eln012  8492  0lt1o  8499  oelim2  8590  oeeulem  8596  oaabs2  8644  cantnff  9665  cnfcom3lem  9694  cfsuc  10248  pf1ind  22196  mavmul0  22376  cramer0  22514  cantnfresb  42563  omabs2  42571  omcl3g  42573  f1omo  47715