Theorem foprab2 4119

Description: Mapping of an operation class abstraction.

Hypothesis

Ref	Expression
foprab2.1	|- F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = C)}

Assertion

Ref	Expression
foprab2	|- (A.x e. A A.y e. B C e. D <-> F:(A X. B)-->D)

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

Proof of Theorem foprab2

Step	Hyp	Ref	Expression
1		fvex 3732	. . . . 5 |- (1st` w) e. V
2		ax-17 971	. . . . 5 |- (z e. (1st` w) -> A.x z e. (1st` w))
3	1, 2	hbcsb1 2025	. . . 4 |- (z e. [_(1st` w) / x]_[_(2nd` w) / y]_C -> A.x z e. [_(1st` w) / x]_[_(2nd` w) / y]_C)
4		ax-17 971	. . . 4 |- (z e. D -> A.x z e. D)
5	3, 4	hbel 1566	. . 3 |- ([_(1st` w) / x]_[_(2nd` w) / y]_C e. D -> A.x[_(1st` w) / x]_[_(2nd` w) / y]_C e. D)
6		ax-17 971	. . . . . 6 |- (z e. (1st` w) -> A.y z e. (1st` w))
7		fvex 3732	. . . . . . 7 |- (2nd` w) e. V
8		ax-17 971	. . . . . . 7 |- (z e. (2nd` w) -> A.y z e. (2nd` w))
9	7, 8	hbcsb1 2025	. . . . . 6 |- (z e. [_(2nd` w) / y]_C -> A.y z e. [_(2nd` w) / y]_C)
10	6, 9	hbcsbg 2026	. . . . 5 |- ((1st` w) e. V -> (z e. [_(1st` w) / x]_[_(2nd` w) / y]_C -> A.y z e. [_(1st` w) / x]_[_(2nd` w) / y]_C))
11	1, 10	ax-mp 7	. . . 4 |- (z e. [_(1st` w) / x]_[_(2nd` w) / y]_C -> A.y z e. [_(1st` w) / x]_[_(2nd` w) / y]_C)
12		ax-17 971	. . . 4 |- (z e. D -> A.y z e. D)
13	11, 12	hbel 1566	. . 3 |- ([_(1st` w) / x]_[_(2nd` w) / y]_C e. D -> A.y[_(1st` w) / x]_[_(2nd` w) / y]_C e. D)
14		ax-17 971	. . 3 |- (C e. D -> A.w C e. D)
15		csbopeq1a 4112	. . . . . 6 |- (<.x, y>. = w -> C = [_(1st` w) / x]_[_(2nd` w) / y]_C)
16	15	eqcoms 1478	. . . . 5 |- (w = <.x, y>. -> C = [_(1st` w) / x]_[_(2nd` w) / y]_C)
17	16	eqcomd 1480	. . . 4 |- (w = <.x, y>. -> [_(1st` w) / x]_[_(2nd` w) / y]_C = C)
18	17	eleq1d 1540	. . 3 |- (w = <.x, y>. -> ([_(1st` w) / x]_[_(2nd` w) / y]_C e. D <-> C e. D))
19	5, 13, 14, 18	ralxpf 3220	. 2 |- (A.w e. (A X. B)[_(1st` w) / x]_[_(2nd` w) / y]_C e. D <-> A.x e. A A.y e. B C e. D)
20		dfoprab3 4114	. . . 4 |- {<.<.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))}
21		foprab2.1	. . . 4 |- F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = C)}
22		anass 439	. . . . . 6 |- (((w e. (V X. V) /\ ((1st` w) e. A /\ (2nd` w) e. B)) /\ z = [_(1st` w) / x]_[_(2nd` w) / y]_C) <-> (w e. (V X. V) /\ (((1st` w) e. A /\ (2nd` w) e. B) /\ z = [_(1st` w) / x]_[_(2nd` w) / y]_C)))
23		elxp7 4103	. . . . . . 7 |- (w e. (A X. B) <-> (w e. (V X. V) /\ ((1st` w) e. A /\ (2nd` w) e. B)))
24	23	anbi1i 481	. . . . . 6 |- ((w e. (A X. B) /\ z = [_(1st` w) / x]_[_(2nd` w) / y]_C) <-> ((w e. (V X. V) /\ ((1st` w) e. A /\ (2nd` w) e. B)) /\ z = [_(1st` w) / x]_[_(2nd` w) / y]_C))
25		sbcang 1971	. . . . . . . . . . . 12 |- ((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)))
26	7, 25	ax-mp 7	. . . . . . . . . . 11 |- ([(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))
27		sbcang 1971	. . . . . . . . . . . . . 14 |- ((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)))
28	7, 27	ax-mp 7	. . . . . . . . . . . . 13 |- ([(2nd` w) / y](x e. A /\ y e. B) <-> ([(2nd` w) / y]x e. A /\ [(2nd` w) / y]y e. B))
29		ax-17 971	. . . . . . . . . . . . . . . 16 |- (x e. A -> A.y x e. A)
30	29	sbcgf 1986	. . . . . . . . . . . . . . 15 |- ((2nd` w) e. V -> ([(2nd` w) / y]x e. A <-> x e. A))
31	7, 30	ax-mp 7	. . . . . . . . . . . . . 14 |- ([(2nd` w) / y]x e. A <-> x e. A)
32		sbcel1gv 1980	. . . . . . . . . . . . . . 15 |- ((2nd` w) e. V -> ([(2nd` w) / y]y e. B <-> (2nd` w) e. B))
33	7, 32	ax-mp 7	. . . . . . . . . . . . . 14 |- ([(2nd` w) / y]y e. B <-> (2nd` w) e. B)
34	31, 33	anbi12i 482	. . . . . . . . . . . . 13 |- (([(2nd` w) / y]x e. A /\ [(2nd` w) / y]y e. B) <-> (x e. A /\ (2nd` w) e. B))
35	28, 34	bitr 173	. . . . . . . . . . . 12 |- ([(2nd` w) / y](x e. A /\ y e. B) <-> (x e. A /\ (2nd` w) e. B))
36		sbceq2dig 2016	. . . . . . . . . . . . 13 |- ((2nd` w) e. V -> ([(2nd` w) / y]z = C <-> z = [_(2nd` w) / y]_C))
37	7, 36	ax-mp 7	. . . . . . . . . . . 12 |- ([(2nd` w) / y]z = C <-> z = [_(2nd` w) / y]_C)
38	35, 37	anbi12i 482	. . . . . . . . . . 11 |- (([(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))
39	26, 38	bitr 173	. . . . . . . . . 10 |- ([(2nd` w) / y]((x e. A /\ y e. B) /\ z = C) <-> ((x e. A /\ (2nd` w) e. B) /\ z = [_(2nd` w) / y]_C))
40	39	sbcbii 1978	. . . . . . . . 9 |- ((1st` w) e. V -> ([(1st` w) / x][(2nd` w) / y]((x e. A /\ y e. B) /\ z = C) <-> [(1st` w) / x]((x e. A /\ (2nd` w) e. B) /\ z = [_(2nd` w) / y]_C)))
41	1, 40	ax-mp 7	. . . . . . . 8 |- ([(1st` w) / x][(2nd` w) / y]((x e. A /\ y e. B) /\ z = C) <-> [(1st` w) / x]((x e. A /\ (2nd` w) e. B) /\ z = [_(2nd` w) / y]_C))
42		sbcang 1971	. . . . . . . . 9 |- ((1st` w) e. V -> ([(1st` w) / x]((x e. A /\ (2nd` w) e. B) /\ z = [_(2nd` w) / y]_C) <-> ([(1st` w) / x](x e. A /\ (2nd` w) e. B) /\ [(1st` w) / x]z = [_(2nd` w) / y]_C)))
43	1, 42	ax-mp 7	. . . . . . . 8 |- ([(1st` w) / x]((x e. A /\ (2nd` w) e. B) /\ z = [_(2nd` w) / y]_C) <-> ([(1st` w) / x](x e. A /\ (2nd` w) e. B) /\ [(1st` w) / x]z = [_(2nd` w) / y]_C))
44		sbcang 1971	. . . . . . . . . . 11 |- ((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)))
45	1, 44	ax-mp 7	. . . . . . . . . 10 |- ([(1st` w) / x](x e. A /\ (2nd` w) e. B) <-> ([(