Theorem eqpw1uni 4330

Description: A class of singletons is equal to the unit power class of its union. (Contributed by SF, 26-Jan-2015.)

Assertion

Ref	Expression
eqpw1uni	|- (A C_ 1c -> A = ~P1 U.A)

Proof of Theorem eqpw1uni

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

Step	Hyp	Ref	Expression
1		ssel 3267	. . 3 |- (A C_ 1c -> (x e. A -> x e. 1c))
2		pw1ss1c 4158	. . . . 5 |- ~P1 U.A C_ 1c
3	2	sseli 3269	. . . 4 |- (x e. ~P1 U.A -> x e. 1c)
4	3	a1i 10	. . 3 |- (A C_ 1c -> (x e. ~P1 U.A -> x e. 1c))
5		el1c 4139	. . . 4 |- (x e. 1c <-> E.y x = {y})
6		vex 2862	. . . . . . . . . 10 |- y e. _V
7	6	snid 3760	. . . . . . . . 9 |- y e. {y}
8		eleq2 2414	. . . . . . . . . 10 |- (x = {y} -> (y e. x <-> y e. {y}))
9	8	rspcev 2955	. . . . . . . . 9 |- (({y} e. A /\ y e. {y}) -> E.x e. A y e. x)
10	7, 9	mpan2 652	. . . . . . . 8 |- ({y} e. A -> E.x e. A y e. x)
11		el1c 4139	. . . . . . . . . . 11 |- (x e. 1c <-> E.z x = {z})
12		elsn 3748	. . . . . . . . . . . . . . 15 |- (y e. {z} <-> y = z)
13		sneq 3744	. . . . . . . . . . . . . . . 16 |- (y = z -> {y} = {z})
14	13	eleq1d 2419	. . . . . . . . . . . . . . 15 |- (y = z -> ({y} e. A <-> {z} e. A))
15	12, 14	sylbi 187	. . . . . . . . . . . . . 14 |- (y e. {z} -> ({y} e. A <-> {z} e. A))
16	15	biimprcd 216	. . . . . . . . . . . . 13 |- ({z} e. A -> (y e. {z} -> {y} e. A))
17		eleq1 2413	. . . . . . . . . . . . . 14 |- (x = {z} -> (x e. A <-> {z} e. A))
18		eleq2 2414	. . . . . . . . . . . . . . 15 |- (x = {z} -> (y e. x <-> y e. {z}))
19	18	imbi1d 308	. . . . . . . . . . . . . 14 |- (x = {z} -> ((y e. x -> {y} e. A) <-> (y e. {z} -> {y} e. A)))
20	17, 19	imbi12d 311	. . . . . . . . . . . . 13 |- (x = {z} -> ((x e. A -> (y e. x -> {y} e. A)) <-> ({z} e. A -> (y e. {z} -> {y} e. A))))
21	16, 20	mpbiri 224	. . . . . . . . . . . 12 |- (x = {z} -> (x e. A -> (y e. x -> {y} e. A)))
22	21	exlimiv 1634	. . . . . . . . . . 11 |- (E.z x = {z} -> (x e. A -> (y e. x -> {y} e. A)))
23	11, 22	sylbi 187	. . . . . . . . . 10 |- (x e. 1c -> (x e. A -> (y e. x -> {y} e. A)))
24	1, 23	syli 33	. . . . . . . . 9 |- (A C_ 1c -> (x e. A -> (y e. x -> {y} e. A)))
25	24	rexlimdv 2737	. . . . . . . 8 |- (A C_ 1c -> (E.x e. A y e. x -> {y} e. A))
26	10, 25	impbid2 195	. . . . . . 7 |- (A C_ 1c -> ({y} e. A <-> E.x e. A y e. x))
27		eluni2 3895	. . . . . . 7 |- (y e. U.A <-> E.x e. A y e. x)
28	26, 27	syl6bbr 254	. . . . . 6 |- (A C_ 1c -> ({y} e. A <-> y e. U.A))
29		eleq1 2413	. . . . . . 7 |- (x = {y} -> (x e. A <-> {y} e. A))
30		eleq1 2413	. . . . . . . 8 |- (x = {y} -> (x e. ~P1 U.A <-> {y} e. ~P1 U.A))
31		snelpw1 4146	. . . . . . . 8 |- ({y} e. ~P1 U.A <-> y e. U.A)
32	30, 31	syl6bb 252	. . . . . . 7 |- (x = {y} -> (x e. ~P1 U.A <-> y e. U.A))
33	29, 32	bibi12d 312	. . . . . 6 |- (x = {y} -> ((x e. A <-> x e. ~P1 U.A) <-> ({y} e. A <-> y e. U.A)))
34	28, 33	syl5ibrcom 213	. . . . 5 |- (A C_ 1c -> (x = {y} -> (x e. A <-> x e. ~P1 U.A)))
35	34	exlimdv 1636	. . . 4 |- (A C_ 1c -> (E.y x = {y} -> (x e. A <-> x e. ~P1 U.A)))
36	5, 35	syl5bi 208	. . 3 |- (A C_ 1c -> (x e. 1c -> (x e. A <-> x e. ~P1 U.A)))
37	1, 4, 36	pm5.21ndd 343	. 2 |- (A C_ 1c -> (x e. A <-> x e. ~P1 U.A))
38	37	eqrdv 2351	1 |- (A C_ 1c -> A = ~P1 U.A)

Syntax hints:   -> wi 4   <-> wb 176  E.wex 1541   = wceq 1642   e. wcel 1710  E.wrex 2615   C_ wss 3257  {csn 3737  U.cuni 3891  1_cc1c 4134  ~P₁ cpw1 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 4078  ax-sn 4087

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 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-ss 3259  df-nul 3551  df-pw 3724  df-sn 3741  df-uni 3892  df-1c 4136  df-pw1 4137

This theorem is referenced by:  pw1equn  4331  pw1eqadj  4332  sspw1  4335  sspw12  4336