elpw11c - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > elpw11c		GIF version

Theorem elpw11c 4148

Description: Membership in ℘₁1_c. (Contributed by SF, 13-Jan-2015.)

**Assertion**
Ref	Expression
elpw11c	⊢ (A ∈ ℘₁1_c ↔ ∃x A = {{x}})

Distinct variable group: x,A

Proof of Theorem elpw11c Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elpw1 4145	. 2 ⊢ (A ∈ ℘₁1_c ↔ ∃y ∈ 1_c A = {y})
2		df-rex 2621	. . 3 ⊢ (∃y ∈ 1_c A = {y} ↔ ∃y(y ∈ 1_c ∧ A = {y}))
3		el1c 4140	. . . . . 6 ⊢ (y ∈ 1_c ↔ ∃x y = {x})
4	3	anbi1i 676	. . . . 5 ⊢ ((y ∈ 1_c ∧ A = {y}) ↔ (∃x y = {x} ∧ A = {y}))
5		19.41v 1901	. . . . 5 ⊢ (∃x(y = {x} ∧ A = {y}) ↔ (∃x y = {x} ∧ A = {y}))
6	4, 5	bitr4i 243	. . . 4 ⊢ ((y ∈ 1_c ∧ A = {y}) ↔ ∃x(y = {x} ∧ A = {y}))
7	6	exbii 1582	. . 3 ⊢ (∃y(y ∈ 1_c ∧ A = {y}) ↔ ∃y∃x(y = {x} ∧ A = {y}))
8	2, 7	bitri 240	. 2 ⊢ (∃y ∈ 1_c A = {y} ↔ ∃y∃x(y = {x} ∧ A = {y}))
9		excom 1741	. . 3 ⊢ (∃y∃x(y = {x} ∧ A = {y}) ↔ ∃x∃y(y = {x} ∧ A = {y}))
10		snex 4112	. . . . 5 ⊢ {x} ∈ V
11		sneq 3745	. . . . . 6 ⊢ (y = {x} → {y} = {{x}})
12	11	eqeq2d 2364	. . . . 5 ⊢ (y = {x} → (A = {y} ↔ A = {{x}}))
13	10, 12	ceqsexv 2895	. . . 4 ⊢ (∃y(y = {x} ∧ A = {y}) ↔ A = {{x}})
14	13	exbii 1582	. . 3 ⊢ (∃x∃y(y = {x} ∧ A = {y}) ↔ ∃x A = {{x}})
15	9, 14	bitri 240	. 2 ⊢ (∃y∃x(y = {x} ∧ A = {y}) ↔ ∃x A = {{x}})
16	1, 8, 15	3bitri 262	1 ⊢ (A ∈ ℘₁1_c ↔ ∃x A = {{x}})

Colors of variables: wff setvar class

Syntax hints: ↔ wb 176 ∧ wa 358 ∃wex 1541 = wceq 1642 ∈ wcel 1710 ∃wrex 2616 {csn 3738 1_cc1c 4135 ℘₁cpw1 4136

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-rex 2621 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-pw 3725 df-sn 3742 df-1c 4137 df-pw1 4138

This theorem is referenced by: elpw121c 4149 insklem 4305 ncfinraiselem2 4481 ncfinlowerlem1 4483 eqtfinrelk 4487 evenodddisjlem1 4516 nnpweqlem1 4523 sfintfinlem1 4532 tfinnnlem1 4534 df1st2 4739 dfswap2 4742