Theorem el1o 8507

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ∅c0 4308  {csn 4601  1_oc1o 8473

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 2707  ax-nul 5276

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-un 3931  df-nul 4309  df-sn 4602  df-suc 6358  df-1o 8480

This theorem is referenced by:  ord1eln01  8508  ord2eln012  8509  0lt1o  8516  oelim2  8607  oeeulem  8613  oaabs2  8661  cantnff  9688  cnfcom3lem  9717  cfsuc  10271  pf1ind  22293  mavmul0  22490  cramer0  22628  cantnfresb  43348  omabs2  43356  omcl3g  43358  f1omo  48868  isinito3  49385