Theorem uniiunlem 2129

Description: A subset relationship useful for converting union to indexed union using dfiun2 2583 or dfiun2g 2582 and intersection to indexed intersection using dfiin2 2584.

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 1685	. . . . 5 |- (A.x e. A B e. C -> A.xA.x e. A B e. C)
2		ax-17 970	. . . . 5 |- (z e. C -> A.x z e. C)
3		ra4 1692	. . . . . 6 |- (A.x e. A B e. C -> (x e. A -> B e. C))
4		eleq1a 1541	. . . . . 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 1743	. . . 4 |- (A.x e. A B e. C -> (E.x e. A z = B -> z e. C))
7	6	19.21aiv 1285	. . 3 |- (A.x e. A B e. C -> A.z(E.x e. A z = B -> z e. C))
8		hbre1 1687	. . . . . . 7 |- (E.x e. A z = B -> A.xE.x e. A z = B)
9	8, 2	hbim 1006	. . . . . 6 |- ((E.x e. A z = B -> z e. C) -> A.x(E.x e. A z = B -> z e. C))
10	9	hbal 1004	. . . . 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 2003	. . . . . . . . . . . 12 |- (x = w -> B = [_w / x]_B)
12	11	eqcoms 1476	. . . . . . . . . . 11 |- (w = x -> B = [_w / x]_B)
13	12	eqcomd 1478	. . . . . . . . . 10 |- (w = x -> [_w / x]_B = B)
14	13	eqeq1d 1481	. . . . . . . . 9 |- (w = x -> ([_w / x]_B = B <-> B = B))
15		eqid 1474	. . . . . . . . 9 |- B = B
16	14, 15	a4eiv 1273	. . . . . . . 8 |- E.w[_w / x]_B = B
17		visset 1810	. . . . . . . . . . . . . . . . . 18 |- w e. V
18		ax-17 970	. . . . . . . . . . . . . . . . . 18 |- (z e. w -> A.x z e. w)
19	17, 18	hbcsb1 2022	. . . . . . . . . . . . . . . . 17 |- (z e. [_w / x]_B -> A.x z e. [_w / x]_B)
20	19	hbeleq 1565	. . . . . . . . . . . . . . . 16 |- (z = [_w / x]_B -> A.x z = [_w / x]_B)
21		eqeq1 1479	. . . . . . . . . . . . . . . 16 |- (z = [_w / x]_B -> (z = B <-> [_w / x]_B = B))
22	20, 21	rexbid 1660	. . . . . . . . . . . . . . 15 |- (z = [_w / x]_B -> (E.x e. A z = B <-> E.x e. A [_w / x]_B = B))
23		eleq1 1532	. . . . . . . . . . . . . . 15 |- (z = [_w / x]_B -> (z e. C <-> [_w / x]_B e. C))
24	22, 23	imbi12d 625	. . . . . . . . . . . . . 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 1859	. . . . . . . . . . . . 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 1693	. . . . . . . . . . . . 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 1532	. . . . . . . . . 10 |- ([_w / x]_B = B -> ([_w / x]_B e. D <-> B e. D))
31		eleq1 1532	. . . . . . . . . . . 12 |- ([_w / x]_B = B -> ([_w / x]_B e. C <-> B e. C))
32	31	imbi2d 611	. . . . . . . . . . 11 |- ([_w / x]_B = B -> ((x e. A -> [_w / x]_B e. C) <-> (x e. A -> B e. C)))
33	32	imbi2d 611	. . . . . . . . . 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 541	. . . . . . . . 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 1294	. . . . . . . 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 1706	. . . 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 517	. 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 2114	. . 3 |- ({z | E.x e. A z = B} (_ C <-> A.z(E.x e. A z = B -> z e. C))
43		eqeq1 1479	. . . . . 6 |- (z = y -> (z = B <-> y = B))
44	43	rexbidv 1662	. . . . 5 |- (z = y -> (E.x e. A z = B <-> E.x e. A y = B))
45	44	cbvabv 1906	. . . 4 |- {z | E.x e. A z = B} = {y | E.x e. A y = B}
46	45	sseq1i 2082	. . 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 535	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 953   = wceq 955   e. wcel 957  E.wex 979  {cab 1462  A.wral 1643  E.wrex 1644  [_csb 1998   (_ wss 2044

This theorem is referenced by:  iunopnt 7559

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-ral 1647  df-rex 1648  df-v 1809  df-sbc 1939  df-csb 1999  df-in 2048  df-ss 2050

Copyright terms: Public domain