Theorem dfoprab5 4115

Description: A way to define an operation class abstraction without using existential quantifiers.

Hypothesis

Ref	Expression
dfoprab5.1	|- (<.x, y>. = w -> C = D)

Assertion

Ref	Expression
dfoprab5	|- {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = C)} = {<.w, z>. | (w e. (A X. B) /\ z = D)}

Distinct variable groups:   x,w,y,A   w,B,x,y   w,C   x,D,y   z,w,x,y

Proof of Theorem dfoprab5

Step	Hyp	Ref	Expression
1		dfoprab3 4114	. 2 |- {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = C)} = {<.w, z>. | (w e. (V X. V) /\ [(1st` w) / x][(2nd` w) / y]((x e. A /\ y e. B) /\ z = C))}
2		anass 439	. . . 4 |- (((w e. (V X. V) /\ ((1st` w) e. A /\ (2nd` w) e. B)) /\ z = D) <-> (w e. (V X. V) /\ (((1st` w) e. A /\ (2nd` w) e. B) /\ z = D)))
3		elxp7 4103	. . . . 5 |- (w e. (A X. B) <-> (w e. (V X. V) /\ ((1st` w) e. A /\ (2nd` w) e. B)))
4	3	anbi1i 481	. . . 4 |- ((w e. (A X. B) /\ z = D) <-> ((w e. (V X. V) /\ ((1st` w) e. A /\ (2nd` w) e. B)) /\ z = D))
5		fvex 3732	. . . . . . . . . 10 |- (1st` w) e. V
6		sbcang 1971	. . . . . . . . . 10 |- ((1st` w) e. V -> ([(1st` w) / x](x e. A /\ (2nd` w) e. B) <-> ([(1st` w) / x]x e. A /\ [(1st` w) / x](2nd` w) e. B)))
7	5, 6	ax-mp 7	. . . . . . . . 9 |- ([(1st` w) / x](x e. A /\ (2nd` w) e. B) <-> ([(1st` w) / x]x e. A /\ [(1st` w) / x](2nd` w) e. B))
8		sbcel1gv 1980	. . . . . . . . . . 11 |- ((1st` w) e. V -> ([(1st` w) / x]x e. A <-> (1st` w) e. A))
9	5, 8	ax-mp 7	. . . . . . . . . 10 |- ([(1st` w) / x]x e. A <-> (1st` w) e. A)
10		ax-17 971	. . . . . . . . . . . 12 |- ((2nd` w) e. B -> A.x(2nd` w) e. B)
11	10	sbcgf 1986	. . . . . . . . . . 11 |- ((1st` w) e. V -> ([(1st` w) / x](2nd` w) e. B <-> (2nd` w) e. B))
12	5, 11	ax-mp 7	. . . . . . . . . 10 |- ([(1st` w) / x](2nd` w) e. B <-> (2nd` w) e. B)
13	9, 12	anbi12i 482	. . . . . . . . 9 |- (([(1st` w) / x]x e. A /\ [(1st` w) / x](2nd` w) e. B) <-> ((1st` w) e. A /\ (2nd` w) e. B))
14	7, 13	bitr 173	. . . . . . . 8 |- ([(1st` w) / x](x e. A /\ (2nd` w) e. B) <-> ((1st` w) e. A /\ (2nd` w) e. B))
15	14	a1i 8	. . . . . . 7 |- (w e. (V X. V) -> ([(1st` w) / x](x e. A /\ (2nd` w) e. B) <-> ((1st` w) e. A /\ (2nd` w) e. B)))
16		visset 1813	. . . . . . . . . . . . . 14 |- y e. V
17	16	eqop 4104	. . . . . . . . . . . . 13 |- (w e. (V X. V) -> (w = <.x, y>. <-> ((1st` w) = x /\ (2nd` w) = y)))
18		eqcom 1477	. . . . . . . . . . . . 13 |- (<.x, y>. = w <-> w = <.x, y>.)
19		eqcom 1477	. . . . . . . . . . . . . 14 |- (x = (1st` w) <-> (1st` w) = x)
20		eqcom 1477	. . . . . . . . . . . . . 14 |- (y = (2nd` w) <-> (2nd` w) = y)
21	19, 20	anbi12i 482	. . . . . . . . . . . . 13 |- ((x = (1st` w) /\ y = (2nd` w)) <-> ((1st` w) = x /\ (2nd` w) = y))
22	17, 18, 21	3bitr4g 555	. . . . . . . . . . . 12 |- (w e. (V X. V) -> (<.x, y>. = w <-> (x = (1st` w) /\ y = (2nd` w))))
23		dfoprab5.1	. . . . . . . . . . . 12 |- (<.x, y>. = w -> C = D)
24	22, 23	syl6bir 215	. . . . . . . . . . 11 |- (w e. (V X. V) -> ((x = (1st` w) /\ y = (2nd` w)) -> C = D))
25	24	19.21aivv 1287	. . . . . . . . . 10 |- (w e. (V X. V) -> A.xA.y((x = (1st` w) /\ y = (2nd` w)) -> C = D))
26		fvex 3732	. . . . . . . . . . 11 |- (2nd` w) e. V
27	5, 26	csbie2t 2033	. . . . . . . . . 10 |- (A.xA.y((x = (1st` w) /\ y = (2nd` w)) -> C = D) -> [_(1st` w) / x]_[_(2nd` w) / y]_C = D)
28	25, 27	syl 10	. . . . . . . . 9 |- (w e. (V X. V) -> [_(1st` w) / x]_[_(2nd` w) / y]_C = D)
29	28	eqeq2d 1486	. . . . . . . 8 |- (w e. (V X. V) -> (z = [_(1st` w) / x]_[_(2nd` w) / y]_C <-> z = D))
30		sbceq2dig 2016	. . . . . . . . 9 |- ((1st` w) e. V -> ([(1st` w) / x]z = [_(2nd` w) / y]_C <-> z = [_(1st` w) / x]_[_(2nd` w) / y]_C))
31	5, 30	ax-mp 7	. . . . . . . 8 |- ([(1st` w) / x]z = [_(2nd` w) / y]_C <-> z = [_(1st` w) / x]_[_(2nd` w) / y]_C)
32	29, 31	syl5bb 532	. . . . . . 7 |- (w e. (V X. V) -> ([(1st` w) / x]z = [_(2nd` w) / y]_C <-> z = D))
33	15, 32	anbi12d 628	. . . . . 6 |- (w e. (V X. V) -> (([(1st` w) / x](x e. A /\ (2nd` w) e. B) /\ [(1st` w) / x]z = [_(2nd` w) / y]_C) <-> (((1st` w) e. A /\ (2nd` w) e. B) /\ z = D)))
34		sbcang 1971	. . . . . . . . . . 11 |- ((2nd` w) e. V -> ([(2nd` w) / y]((x e. A /\ y e. B) /\ z = C) <-> ([(2nd` w) / y](x e. A /\ y e. B) /\ [(2nd` w) / y]z = C)))
35	26, 34	ax-mp 7	. . . . . . . . . 10 |- ([(2nd` w) / y]((x e. A /\ y e. B) /\ z = C) <-> ([(2nd` w) / y](x e. A /\ y e. B) /\ [(2nd` w) / y]z = C))
36		sbcang 1971	. . . . . . . . . . . . 13 |- ((2nd` w) e. V -> ([(2nd` w) / y](x e. A /\ y e. B) <-> ([(2nd` w) / y]x e. A /\ [(2nd` w) / y]y e. B)))
37	26, 36	ax-mp 7	. . . . . . . . . . . 12 |- ([(2nd` w) / y](x e. A /\ y e. B) <-> ([(2nd` w) / y]x e. A /\ [(2nd` w) / y]y e. B))
38		ax-17 971	. . . . . . . . . . . . . . 15 |- (x e. A -> A.y x e. A)
39	38	sbcgf 1986	. . . . . . . . . . . . . 14 |- ((2nd` w) e. V -> ([(2nd` w) / y]x e. A <-> x e. A))
40	26, 39	ax-mp 7	. . . . . . . . . . . . 13 |- ([(2nd` w) / y]x e. A <-> x e. A)
41		sbcel1gv 1980	. . . . . . . . . . . . . 14 |- ((2nd` w) e. V -> ([(2nd` w) / y]y e. B <-> (2nd` w) e. B))
42	26, 41	ax-mp 7	. . . . . . . . . . . . 13 |- ([(2nd` w) / y]y e. B <-> (2nd` w) e. B)
43	40, 42	anbi12i 482	. . . . . . . . . . . 12 |- (([(2nd` w) / y]x e. A /\ [(2nd` w) / y]y e. B) <-> (x e. A /\ (2nd` w) e. B))
44	37, 43	bitr 173	. . . . . . . . . . 11 |- ([(2nd` w) / y](x e. A /\ y e. B) <-> (x e. A /\ (2nd` w) e. B))
45		sbceq2dig 2016	. . . . . . . . . . . 12 |- ((2nd` w) e. V -> ([(2nd` w) / y]z = C <-> z = [_(2nd` w) / y]_C))
46	26, 45	ax-mp 7	. . . . . . . . . . 11 |- ([(2nd` w) / y]z = C <-> z = [_(2nd` w) / y]_C)
47	44, 46	anbi12i 482	. . . . . . . . . 10 |- (([(2nd` w) / y](x e. A /\ y e. B) /\ [(2nd` w) / y]z = C) <-> ((x e. A /\ (2nd` w) e. B) /\ z = [_(2nd` w) / y]_C))
48	35, 47	bitr 173	. . . . . . . . 9 |- ([(2nd` w) / y]((x e. A /\ y e. B) /\ z = C) <-> ((x e. A /\ (2nd` w) e. B) /\ z = [_(2nd` w) / y]_C))
49	48	sbcbii 1978	. . . . . . . 8 |- ((1st` w) e. V -> ([(1st` w) / x][(2nd` w) / y]((x e. A /\ y e. B) /\ z = C) <-> [(1st`