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	|- U.~P1 A = 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 e. U.~P1 A <-> E.y(x e. y /\ y e. ~P1 A))
2		elpw1 4145	. . . . . 6 |- (y e. ~P1 A <-> E.z e. A y = {z})
3	2	anbi1i 676	. . . . 5 |- ((y e. ~P1 A /\ x e. y) <-> (E.z e. A y = {z} /\ x e. y))
4		ancom 437	. . . . 5 |- ((x e. y /\ y e. ~P1 A) <-> (y e. ~P1 A /\ x e. y))
5		r19.41v 2765	. . . . 5 |- (E.z e. A (y = {z} /\ x e. y) <-> (E.z e. A y = {z} /\ x e. y))
6	3, 4, 5	3bitr4i 268	. . . 4 |- ((x e. y /\ y e. ~P1 A) <-> E.z e. A (y = {z} /\ x e. y))
7	6	exbii 1582	. . 3 |- (E.y(x e. y /\ y e. ~P1 A) <-> E.yE.z e. A (y = {z} /\ x e. y))
8		risset 2662	. . . 4 |- (x e. A <-> E.z e. A z = x)
9		snex 4112	. . . . . . 7 |- {z} e. _V
10		eleq2 2414	. . . . . . 7 |- (y = {z} -> (x e. y <-> x e. {z}))
11	9, 10	ceqsexv 2895	. . . . . 6 |- (E.y(y = {z} /\ x e. y) <-> x e. {z})
12		df-sn 3742	. . . . . . 7 |- {z} = {x | x = z}
13	12	eqabri 2461	. . . . . 6 |- (x e. {z} <-> x = z)
14		equcom 1680	. . . . . 6 |- (x = z <-> z = x)
15	11, 13, 14	3bitri 262	. . . . 5 |- (E.y(y = {z} /\ x e. y) <-> z = x)
16	15	rexbii 2640	. . . 4 |- (E.z e. A E.y(y = {z} /\ x e. y) <-> E.z e. A z = x)
17		rexcom4 2879	. . . 4 |- (E.z e. A E.y(y = {z} /\ x e. y) <-> E.yE.z e. A (y = {z} /\ x e. y))
18	8, 16, 17	3bitr2ri 265	. . 3 |- (E.yE.z e. A (y = {z} /\ x e. y) <-> x e. A)
19	1, 7, 18	3bitri 262	. 2 |- (x e. U.~P1 A <-> x e. A)
20	19	eqriv 2350	1 |- U.~P1 A = A

Syntax hints:   /\ wa 358  E.wex 1541   = wceq 1642   e. wcel 1710  E.wrex 2616  {csn 3738  U.cuni 3892  ~P₁ 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