Theorem unipw1 4326

Description: The union of a unit power class is the original set. (Contributed by SF, 20-Jan-2015.)

Assertion

Ref	Expression
unipw1	⊢ ∪℘1A = A

Proof of Theorem unipw1

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eluni 3895	. . 3 ⊢ (x ∈ ∪℘1A ↔ ∃y(x ∈ y ∧ y ∈ ℘1A))
2		elpw1 4145	. . . . . 6 ⊢ (y ∈ ℘1A ↔ ∃z ∈ A y = {z})
3	2	anbi1i 676	. . . . 5 ⊢ ((y ∈ ℘1A ∧ x ∈ y) ↔ (∃z ∈ A y = {z} ∧ x ∈ y))
4		ancom 437	. . . . 5 ⊢ ((x ∈ y ∧ y ∈ ℘1A) ↔ (y ∈ ℘1A ∧ x ∈ y))
5		r19.41v 2765	. . . . 5 ⊢ (∃z ∈ A (y = {z} ∧ x ∈ y) ↔ (∃z ∈ A y = {z} ∧ x ∈ y))
6	3, 4, 5	3bitr4i 268	. . . 4 ⊢ ((x ∈ y ∧ y ∈ ℘1A) ↔ ∃z ∈ A (y = {z} ∧ x ∈ y))
7	6	exbii 1582	. . 3 ⊢ (∃y(x ∈ y ∧ y ∈ ℘1A) ↔ ∃y∃z ∈ A (y = {z} ∧ x ∈ y))
8		risset 2662	. . . 4 ⊢ (x ∈ A ↔ ∃z ∈ A z = x)
9		snex 4112	. . . . . . 7 ⊢ {z} ∈ V
10		eleq2 2414	. . . . . . 7 ⊢ (y = {z} → (x ∈ y ↔ x ∈ {z}))
11	9, 10	ceqsexv 2895	. . . . . 6 ⊢ (∃y(y = {z} ∧ x ∈ y) ↔ x ∈ {z})
12		df-sn 3742	. . . . . . 7 ⊢ {z} = {x ∣ x = z}
13	12	abeq2i 2461	. . . . . 6 ⊢ (x ∈ {z} ↔ x = z)
14		equcom 1680	. . . . . 6 ⊢ (x = z ↔ z = x)
15	11, 13, 14	3bitri 262	. . . . 5 ⊢ (∃y(y = {z} ∧ x ∈ y) ↔ z = x)
16	15	rexbii 2640	. . . 4 ⊢ (∃z ∈ A ∃y(y = {z} ∧ x ∈ y) ↔ ∃z ∈ A z = x)
17		rexcom4 2879	. . . 4 ⊢ (∃z ∈ A ∃y(y = {z} ∧ x ∈ y) ↔ ∃y∃z ∈ A (y = {z} ∧ x ∈ y))
18	8, 16, 17	3bitr2ri 265	. . 3 ⊢ (∃y∃z ∈ A (y = {z} ∧ x ∈ y) ↔ x ∈ A)
19	1, 7, 18	3bitri 262	. 2 ⊢ (x ∈ ∪℘1A ↔ x ∈ A)
20	19	eqriv 2350	1 ⊢ ∪℘1A = A

Syntax hints:   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  ∃wrex 2616  {csn 3738  ∪cuni 3892  ℘₁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-uni 3893  df-1c 4137  df-pw1 4138

This theorem is referenced by:  pw1exb  4327  pw1equn  4332  pw1eqadj  4333  sspw1  4336