Theorem el1o 8420

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∅c0 4286  {csn 4579  1_oc1o 8388

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-dif 3908  df-un 3910  df-nul 4287  df-sn 4580  df-suc 6317  df-1o 8395

This theorem is referenced by:  ord1eln01  8421  ord2eln012  8422  0lt1o  8429  oelim2  8520  oeeulem  8526  oaabs2  8574  cantnff  9589  cnfcom3lem  9618  cfsuc  10170  pf1ind  22259  mavmul0  22456  cramer0  22594  cantnfresb  43317  omabs2  43325  omcl3g  43327  f1omoOLD  48898  isinito3  49505