Theorem mpt2eq123 5661

Description: An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)

Assertion

Ref	Expression
mpt2eq123	|- ((A = D /\ A.x e. A (B = E /\ A.y e. B C = F)) -> (x e. A, y e. B |-> C) = (x e. D, y e. E |-> F))

Distinct variable groups:   x,y,A   y,B   x,D,y   y,E

Allowed substitution hints:   B(x)   C(x,y)   E(x)   F(x,y)

Proof of Theorem mpt2eq123

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1619	. . . 4 |- F/x A = D
2		nfra1 2664	. . . 4 |- F/xA.x e. A (B = E /\ A.y e. B C = F)
3	1, 2	nfan 1824	. . 3 |- F/x(A = D /\ A.x e. A (B = E /\ A.y e. B C = F))
4		nfv 1619	. . . 4 |- F/y A = D
5		nfcv 2489	. . . . 5 |- F/_yA
6		nfv 1619	. . . . . 6 |- F/y B = E
7		nfra1 2664	. . . . . 6 |- F/yA.y e. B C = F
8	6, 7	nfan 1824	. . . . 5 |- F/y(B = E /\ A.y e. B C = F)
9	5, 8	nfral 2667	. . . 4 |- F/yA.x e. A (B = E /\ A.y e. B C = F)
10	4, 9	nfan 1824	. . 3 |- F/y(A = D /\ A.x e. A (B = E /\ A.y e. B C = F))
11		nfv 1619	. . 3 |- F/z(A = D /\ A.x e. A (B = E /\ A.y e. B C = F))
12		rsp 2674	. . . . . . 7 |- (A.x e. A (B = E /\ A.y e. B C = F) -> (x e. A -> (B = E /\ A.y e. B C = F)))
13		rsp 2674	. . . . . . . . . 10 |- (A.y e. B C = F -> (y e. B -> C = F))
14		eqeq2 2362	. . . . . . . . . 10 |- (C = F -> (z = C <-> z = F))
15	13, 14	syl6 29	. . . . . . . . 9 |- (A.y e. B C = F -> (y e. B -> (z = C <-> z = F)))
16	15	pm5.32d 620	. . . . . . . 8 |- (A.y e. B C = F -> ((y e. B /\ z = C) <-> (y e. B /\ z = F)))
17		eleq2 2414	. . . . . . . . 9 |- (B = E -> (y e. B <-> y e. E))
18	17	anbi1d 685	. . . . . . . 8 |- (B = E -> ((y e. B /\ z = F) <-> (y e. E /\ z = F)))
19	16, 18	sylan9bbr 681	. . . . . . 7 |- ((B = E /\ A.y e. B C = F) -> ((y e. B /\ z = C) <-> (y e. E /\ z = F)))
20	12, 19	syl6 29	. . . . . 6 |- (A.x e. A (B = E /\ A.y e. B C = F) -> (x e. A -> ((y e. B /\ z = C) <-> (y e. E /\ z = F))))
21	20	pm5.32d 620	. . . . 5 |- (A.x e. A (B = E /\ A.y e. B C = F) -> ((x e. A /\ (y e. B /\ z = C)) <-> (x e. A /\ (y e. E /\ z = F))))
22		eleq2 2414	. . . . . 6 |- (A = D -> (x e. A <-> x e. D))
23	22	anbi1d 685	. . . . 5 |- (A = D -> ((x e. A /\ (y e. E /\ z = F)) <-> (x e. D /\ (y e. E /\ z = F))))
24	21, 23	sylan9bbr 681	. . . 4 |- ((A = D /\ A.x e. A (B = E /\ A.y e. B C = F)) -> ((x e. A /\ (y e. B /\ z = C)) <-> (x e. D /\ (y e. E /\ z = F))))
25		anass 630	. . . 4 |- (((x e. A /\ y e. B) /\ z = C) <-> (x e. A /\ (y e. B /\ z = C)))
26		anass 630	. . . 4 |- (((x e. D /\ y e. E) /\ z = F) <-> (x e. D /\ (y e. E /\ z = F)))
27	24, 25, 26	3bitr4g 279	. . 3 |- ((A = D /\ A.x e. A (B = E /\ A.y e. B C = F)) -> (((x e. A /\ y e. B) /\ z = C) <-> ((x e. D /\ y e. E) /\ z = F)))
28	3, 10, 11, 27	oprabbid 5563	. 2 |- ((A = D /\ A.x e. A (B = E /\ A.y e. B C = F)) -> {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = C)} = {<.<.x, y>., z>. | ((x e. D /\ y e. E) /\ z = F)})
29		df-mpt2 5654	. 2 |- (x e. A, y e. B |-> C) = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = C)}
30		df-mpt2 5654	. 2 |- (x e. D, y e. E |-> F) = {<.<.x, y>., z>. | ((x e. D /\ y e. E) /\ z = F)}
31	28, 29, 30	3eqtr4g 2410	1 |- ((A = D /\ A.x e. A (B = E /\ A.y e. B C = F)) -> (x e. A, y e. B |-> C) = (x e. D, y e. E |-> F))

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358   = wceq 1642   e. wcel 1710  A.wral 2614  {coprab 5527   |-> cmpt2 5653

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

This theorem depends on definitions:  df-bi 177  df-an 360  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-ral 2619  df-oprab 5528  df-mpt2 5654

This theorem is referenced by:  mpt2eq12  5662