Theorem el1c 4140

Description: Membership in cardinal one. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
el1c	⊢ (A ∈ 1c ↔ ∃x A = {x})

Distinct variable group:   x,A

Proof of Theorem el1c

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2868	. 2 ⊢ (A ∈ 1c → A ∈ V)
2		snex 4112	. . . 4 ⊢ {x} ∈ V
3		eleq1 2413	. . . 4 ⊢ (A = {x} → (A ∈ V ↔ {x} ∈ V))
4	2, 3	mpbiri 224	. . 3 ⊢ (A = {x} → A ∈ V)
5	4	exlimiv 1634	. 2 ⊢ (∃x A = {x} → A ∈ V)
6		eqeq1 2359	. . . 4 ⊢ (y = A → (y = {x} ↔ A = {x}))
7	6	exbidv 1626	. . 3 ⊢ (y = A → (∃x y = {x} ↔ ∃x A = {x}))
8		df-1c 4137	. . 3 ⊢ 1c = {y ∣ ∃x y = {x}}
9	7, 8	elab2g 2988	. 2 ⊢ (A ∈ V → (A ∈ 1c ↔ ∃x A = {x}))
10	1, 5, 9	pm5.21nii 342	1 ⊢ (A ∈ 1c ↔ ∃x A = {x})

Syntax hints:   ↔ wb 176  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2860  {csn 3738  1_cc1c 4135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-ss 3260  df-nul 3552  df-sn 3742  df-1c 4137

This theorem is referenced by:  snel1c  4141  elpw1  4145  elpw11c  4148  0nel1c  4160  eqpw1  4163  df1c2  4169  pw111  4171  eluni1g  4173  opkelimagekg  4272  sikexlem  4296  dfimak2  4299  dfpw2  4328  eqpw1uni  4331  pw1eqadj  4333  dfeu2  4334  dfnnc2  4396  0nelsuc  4401  elsuc  4414  nnsucelrlem1  4425  nnsucelr  4429  ssfin  4471  nnadjoinlem1  4520  sfintfinlem1  4532  spfinex  4538  elimapw11c  4949  pw1fnf1o  5856  1cnc  6140  el2c  6192