Theorem uniiunlem 2132

Description: A subset relationship useful for converting union to indexed union using dfiun2 2587 or dfiun2g 2586 and intersection to indexed intersection using dfiin2 2588.

Assertion

Ref	Expression
uniiunlem	|- (A.x e. A B e. D -> (A.x e. A B e. C <-> {y | E.x e. A y = B} (_ C))

Distinct variable groups:   y,A   y,B   x,C   x,y

Proof of Theorem uniiunlem

Step	Hyp	Ref	Expression
1		hbra1 1687	. . . . 5 |- (A.x e. A B e. C -> A.xA.x e. A B e. C)
2		ax-17 971	. . . . 5 |- (z e. C -> A.x z e. C)
3		ra4 1694	. . . . . 6 |- (A.x e. A B e. C -> (x e. A -> B e. C))
4		eleq1a 1543	. . . . . 6 |- (B e. C -> (z = B -> z e. C))
5	3, 4	syl6 22	. . . . 5 |- (A.x e. A B e. C -> (x e. A -> (z = B -> z e. C)))
6	1, 2, 5	r19.23ad 1745	. . . 4 |- (A.x e. A B e. C -> (E.x e. A z = B -> z e. C))
7	6	19.21aiv 1286	. . 3 |- (A.x e. A B e. C -> A.z(E.x e. A z = B -> z e. C))
8		hbre1 1689	. . . . . . 7 |- (E.x e. A z = B -> A.xE.x e. A z = B)
9	8, 2	hbim 1007	. . . . . 6 |- ((E.x e. A z = B -> z e. C) -> A.x(E.x e. A z = B -> z e. C))
10	9	hbal 1005	. . . . 5 |- (A.z(E.x e. A z = B -> z e. C) -> A.xA.z(E.x e. A z = B -> z e. C))
11		csbeq1a 2006	. . . . . . . . . . . 12 |- (x = w -> B = [_w / x]_B)
12	11	eqcoms 1478	. . . . . . . . . . 11 |- (w = x -> B = [_w / x]_B)
13	12	eqcomd 1480	. . . . . . . . . 10 |- (w = x -> [_w / x]_B = B)
14	13	eqeq1d 1483	. . . . . . . . 9 |- (w = x -> ([_w / x]_B = B <-> B = B))
15		eqid 1475	. . . . . . . . 9 |- B = B
16	14, 15	a4eiv 1274	. . . . . . . 8 |- E.w[_w / x]_B = B
17		visset 1813	. . . . . . . . . . . . . . . . . 18 |- w e. V
18		ax-17 971	. . . . . . . . . . . . . . . . . 18 |- (z e. w -> A.x z e. w)
19	17, 18	hbcsb1 2025	. . . . . . . . . . . . . . . . 17 |- (z e. [_w / x]_B -> A.x z e. [_w / x]_B)
20	19	hbeleq 1567	. . . . . . . . . . . . . . . 16 |- (z = [_w / x]_B -> A.x z = [_w / x]_B)
21		eqeq1 1481	. . . . . . . . . . . . . . . 16 |- (z = [_w / x]_B -> (z = B <-> [_w / x]_B = B))
22	20, 21	rexbid 1662	. . . . . . . . . . . . . . 15 |- (z = [_w / x]_B -> (E.x e. A z = B <-> E.x e. A [_w / x]_B = B))
23		eleq1 1534	. . . . . . . . . . . . . . 15 |- (z = [_w / x]_B -> (z e. C <-> [_w / x]_B e. C))
24	22, 23	imbi12d 626	. . . . . . . . . . . . . 14 |- (z = [_w / x]_B -> ((E.x e. A z = B -> z e. C) <-> (E.x e. A [_w / x]_B = B -> [_w / x]_B e. C)))
25	24	cla4gv 1862	. . . . . . . . . . . . 13 |- ([_w / x]_B e. D -> (A.z(E.x e. A z = B -> z e. C) -> (E.x e. A [_w / x]_B = B -> [_w / x]_B e. C)))
26		ra4e 1695	. . . . . . . . . . . . 13 |- ((x e. A /\ [_w / x]_B = B) -> E.x e. A [_w / x]_B = B)
27	25, 26	syl7 23	. . . . . . . . . . . 12 |- ([_w / x]_B e. D -> (A.z(E.x e. A z = B -> z e. C) -> ((x e. A /\ [_w / x]_B = B) -> [_w / x]_B e. C)))
28	27	exp4a 378	. . . . . . . . . . 11 |- ([_w / x]_B e. D -> (A.z(E.x e. A z = B -> z e. C) -> (x e. A -> ([_w / x]_B = B -> [_w / x]_B e. C))))
29	28	com4r 41	. . . . . . . . . 10 |- ([_w / x]_B = B -> ([_w / x]_B e. D -> (A.z(E.x e. A z = B -> z e. C) -> (x e. A -> [_w / x]_B e. C))))
30		eleq1 1534	. . . . . . . . . 10 |- ([_w / x]_B = B -> ([_w / x]_B e. D <-> B e. D))
31		eleq1 1534	. . . . . . . . . . . 12 |- ([_w / x]_B = B -> ([_w / x]_B e. C <-> B e. C))
32	31	imbi2d 612	. . . . . . . . . . 11 |- ([_w / x]_B = B -> ((x e. A -> [_w / x]_B e. C) <-> (x e. A -> B e. C)))
33	32	imbi2d 612	. . . . . . . . . 10 |- ([_w / x]_B = B -> ((A.z(E.x e. A z = B -> z e. C) -> (x e. A -> [_w / x]_B e. C)) <-> (A.z(E.x e. A z = B -> z e. C) -> (x e. A -> B e. C))))
34	29, 30, 33	3imtr3d 542	. . . . . . . . 9 |- ([_w / x]_B = B -> (B e. D -> (A.z(E.x e. A z = B -> z e. C) -> (x e. A -> B e. C))))
35	34	19.23aiv 1295	. . . . . . . 8 |- (E.w[_w / x]_B = B -> (B e. D -> (A.z(E.x e. A z = B -> z e. C) -> (x e. A -> B e. C))))
36	16, 35	ax-mp 7	. . . . . . 7 |- (B e. D -> (A.z(E.x e. A z = B -> z e. C) -> (x e. A -> B e. C)))
37	36	imp3a 361	. . . . . 6 |- (B e. D -> ((A.z(E.x e. A z = B -> z e. C) /\ x e. A) -> B e. C))
38	37	com12 11	. . . . 5 |- ((A.z(E.x e. A z = B -> z e. C) /\ x e. A) -> (B e. D -> B e. C))
39	10, 38	r19.20da 1708	. . . 4 |- (A.z(E.x e. A z = B -> z e. C) -> (A.x e. A B e. D -> A.x e. A B e. C))
40	39	com12 11	. . 3 |- (A.x e. A B e. D -> (A.z(E.x e. A z = B -> z e. C) -> A.x e. A B e. C))
41	7, 40	impbid2 518	. 2 |- (A.x e. A B e. D -> (A.x e. A B e. C <-> A.z(E.x e. A z = B -> z e. C)))
42		abss 2117	. . 3 |- ({z | E.x e. A z = B} (_ C <-> A.z(E.x e. A z = B -> z e. C))
43		eqeq1 1481	. . . . . 6 |- (z = y -> (z = B <-> y = B))
44	43	rexbidv 1664	. . . . 5 |- (z = y -> (E.x e. A z = B <-> E.x e. A y = B))
45	44	cbvabv 1909	. . . 4 |- {z | E.x e. A z = B} = {y | E.x e. A y = B}
46	45	sseq1i 2085	. . 3 |- ({z | E.x e. A z = B} (_ C <-> {y | E.x e. A y = B} (_ C)
47	42, 46	bitr3 175	. 2 |- (A.z(E.x e. A z = B -> z e. C) <-> {y | E.x e. A y = B} (_ C)
48	41, 47	syl6bb 536	1 |- (A.x e. A B e. D -> (A.x e. A B e. C <-> {y | E.x e. A y = B} (_ C))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 954   = wceq 956   e. wcel 958  E.wex 980  {cab 1463  A.wral 1645  E.wrex 1646  [_csb 2001   (_ wss 2047

This theorem is referenced by:  iunopnt 7599

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ral 1649  df-rex 1650  df-v 1812  df-sbc 1942  df-csb 2002  df-in 2051  df-ss 2053

Copyright terms: Public domain