Metamath Proof Explorer

Theorem mptbi12f

Description: Equality deduction for maps-to notations. (Contributed by Giovanni Mascellani, 10-Apr-2018)

Ref Expression
Hypotheses mptbi12f.1 
|- F/_ x A
mptbi12f.2 
|- F/_ x B
Assertion mptbi12f 
|- ( ( A = B /\ A. x e. A D = E ) -> ( x e. A |-> D ) = ( x e. B |-> E ) )

Proof

Step Hyp Ref Expression
1 mptbi12f.1 
 |-  F/_ x A
2 mptbi12f.2 
 |-  F/_ x B
3 1 2 nfeq 
 |-  F/ x A = B
4 eleq2 
 |-  ( A = B -> ( x e. A <-> x e. B ) )
5 3 4 alrimi 
 |-  ( A = B -> A. x ( x e. A <-> x e. B ) )
6 ax-5 
 |-  ( ( x e. A <-> x e. B ) -> A. y ( x e. A <-> x e. B ) )
7 5 6 sylg 
 |-  ( A = B -> A. x A. y ( x e. A <-> x e. B ) )
8 eqeq2 
 |-  ( D = E -> ( y = D <-> y = E ) )
9 8 alrimiv 
 |-  ( D = E -> A. y ( y = D <-> y = E ) )
10 9 ralimi 
 |-  ( A. x e. A D = E -> A. x e. A A. y ( y = D <-> y = E ) )
11 df-ral 
 |-  ( A. x e. A A. y ( y = D <-> y = E ) <-> A. x ( x e. A -> A. y ( y = D <-> y = E ) ) )
12 10 11 sylib 
 |-  ( A. x e. A D = E -> A. x ( x e. A -> A. y ( y = D <-> y = E ) ) )
13 19.21v 
 |-  ( A. y ( x e. A -> ( y = D <-> y = E ) ) <-> ( x e. A -> A. y ( y = D <-> y = E ) ) )
14 13 albii 
 |-  ( A. x A. y ( x e. A -> ( y = D <-> y = E ) ) <-> A. x ( x e. A -> A. y ( y = D <-> y = E ) ) )
15 12 14 sylibr 
 |-  ( A. x e. A D = E -> A. x A. y ( x e. A -> ( y = D <-> y = E ) ) )
16 id 
 |-  ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) )
17 16 alanimi 
 |-  ( ( A. y ( x e. A <-> x e. B ) /\ A. y ( x e. A -> ( y = D <-> y = E ) ) ) -> A. y ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) )
18 17 alanimi 
 |-  ( ( A. x A. y ( x e. A <-> x e. B ) /\ A. x A. y ( x e. A -> ( y = D <-> y = E ) ) ) -> A. x A. y ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) )
19 7 15 18 syl2an 
 |-  ( ( A = B /\ A. x e. A D = E ) -> A. x A. y ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) )
20 tsan2 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( x e. A \/ -. ( x e. A /\ y = D ) ) )
21 20 ord 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. x e. A -> -. ( x e. A /\ y = D ) ) )
22 tsbi2 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( ( ( x e. A /\ y = D ) \/ ( x e. B /\ y = E ) ) \/ ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) )
23 22 ord 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. ( ( x e. A /\ y = D ) \/ ( x e. B /\ y = E ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) )
24 23 a1dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. ( ( x e. A /\ y = D ) \/ ( x e. B /\ y = E ) ) -> ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) ) )
25 ax-1 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. ( ( x e. A /\ y = D ) \/ ( x e. B /\ y = E ) ) -> -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) ) )
26 24 25 contrd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( ( x e. A /\ y = D ) \/ ( x e. B /\ y = E ) ) )
27 26 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. x e. A -> ( ( x e. A /\ y = D ) \/ ( x e. B /\ y = E ) ) ) )
28 21 27 cnf1dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. x e. A -> ( x e. B /\ y = E ) ) )
29 simplim 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) )
30 29 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. ( x e. A \/ -. x e. B ) -> ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) ) )
31 tsbi3 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( ( x e. A \/ -. x e. B ) \/ -. ( x e. A <-> x e. B ) ) )
32 31 ord 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. ( x e. A \/ -. x e. B ) -> -. ( x e. A <-> x e. B ) ) )
33 tsan2 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( ( x e. A <-> x e. B ) \/ -. ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) ) )
34 33 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. ( x e. A \/ -. x e. B ) -> ( ( x e. A <-> x e. B ) \/ -. ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) ) ) )
35 32 34 cnf1dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. ( x e. A \/ -. x e. B ) -> -. ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) ) )
36 30 35 contrd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( x e. A \/ -. x e. B ) )
37 36 ord 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. x e. A -> -. x e. B ) )
38 tsan2 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( x e. B \/ -. ( x e. B /\ y = E ) ) )
39 38 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. x e. A -> ( x e. B \/ -. ( x e. B /\ y = E ) ) ) )
40 37 39 cnf1dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. x e. A -> -. ( x e. B /\ y = E ) ) )
41 28 40 contrd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> x e. A )
42 41 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> x e. A ) )
43 29 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) ) )
44 tsan3 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( ( x e. A -> ( y = D <-> y = E ) ) \/ -. ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) ) )
45 44 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> ( ( x e. A -> ( y = D <-> y = E ) ) \/ -. ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) ) ) )
46 43 45 cnfn2dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> ( x e. A -> ( y = D <-> y = E ) ) ) )
47 42 46 mpdd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> ( y = D <-> y = E ) ) )
48 notnotr 
 |-  ( -. -. ( x e. B /\ y = E ) -> ( x e. B /\ y = E ) )
49 48 a1i 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> ( x e. B /\ y = E ) ) )
50 38 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> ( x e. B \/ -. ( x e. B /\ y = E ) ) ) )
51 49 50 cnfn2dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> x e. B ) )
52 36 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> ( x e. A \/ -. x e. B ) ) )
53 51 52 cnfn2dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> x e. A ) )
54 tsan3 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( y = E \/ -. ( x e. B /\ y = E ) ) )
55 54 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> ( y = E \/ -. ( x e. B /\ y = E ) ) ) )
56 49 55 cnfn2dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> y = E ) )
57 29 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) ) )
58 44 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> ( ( x e. A -> ( y = D <-> y = E ) ) \/ -. ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) ) ) )
59 57 58 cnfn2dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> ( x e. A -> ( y = D <-> y = E ) ) ) )
60 53 59 mpdd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> ( y = D <-> y = E ) ) )
61 tsbi3 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( ( y = D \/ -. y = E ) \/ -. ( y = D <-> y = E ) ) )
62 61 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> ( ( y = D \/ -. y = E ) \/ -. ( y = D <-> y = E ) ) ) )
63 60 62 cnfn2dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> ( y = D \/ -. y = E ) ) )
64 56 63 cnfn2dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> y = D ) )
65 53 64 jcad 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> ( x e. A /\ y = D ) ) )
66 ax-1 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) ) )
67 tsim3 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) \/ ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) ) )
68 67 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> ( -. ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) \/ ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) ) ) )
69 66 68 cnf2dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> -. ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) )
70 tsbi1 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( ( -. ( x e. A /\ y = D ) \/ -. ( x e. B /\ y = E ) ) \/ ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) )
71 70 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> ( ( -. ( x e. A /\ y = D ) \/ -. ( x e. B /\ y = E ) ) \/ ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) ) )
72 69 71 cnf2dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> ( -. ( x e. A /\ y = D ) \/ -. ( x e. B /\ y = E ) ) ) )
73 49 72 cnfn2dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. -. ( x e. B /\ y = E ) -> -. ( x e. A /\ y = D ) ) )
74 65 73 contrd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> -. ( x e. B /\ y = E ) )
75 74 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> -. ( x e. B /\ y = E ) ) )
76 26 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> ( ( x e. A /\ y = D ) \/ ( x e. B /\ y = E ) ) ) )
77 75 76 cnf2dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> ( x e. A /\ y = D ) ) )
78 tsan3 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( y = D \/ -. ( x e. A /\ y = D ) ) )
79 78 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> ( y = D \/ -. ( x e. A /\ y = D ) ) ) )
80 77 79 cnfn2dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> y = D ) )
81 33 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> ( ( x e. A <-> x e. B ) \/ -. ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) ) ) )
82 43 81 cnfn2dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> ( x e. A <-> x e. B ) ) )
83 tsbi4 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( ( -. x e. A \/ x e. B ) \/ -. ( x e. A <-> x e. B ) ) )
84 83 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> ( ( -. x e. A \/ x e. B ) \/ -. ( x e. A <-> x e. B ) ) ) )
85 82 84 cnfn2dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> ( -. x e. A \/ x e. B ) ) )
86 42 85 cnfn1dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> x e. B ) )
87 tsan1 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( ( -. x e. B \/ -. y = E ) \/ ( x e. B /\ y = E ) ) )
88 87 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> ( ( -. x e. B \/ -. y = E ) \/ ( x e. B /\ y = E ) ) ) )
89 75 88 cnf2dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> ( -. x e. B \/ -. y = E ) ) )
90 86 89 cnfn1dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> -. y = E ) )
91 tsbi4 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( ( -. y = D \/ y = E ) \/ -. ( y = D <-> y = E ) ) )
92 91 a1d 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> ( ( -. y = D \/ y = E ) \/ -. ( y = D <-> y = E ) ) ) )
93 92 or32dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> ( ( -. y = D \/ -. ( y = D <-> y = E ) ) \/ y = E ) ) )
94 90 93 cnf2dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> ( -. y = D \/ -. ( y = D <-> y = E ) ) ) )
95 80 94 cnfn1dd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> ( -. F. -> -. ( y = D <-> y = E ) ) )
96 47 95 contrd 
 |-  ( -. ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) ) -> F. )
97 96 efald2 
 |-  ( ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) )
98 97 2alimi 
 |-  ( A. x A. y ( ( x e. A <-> x e. B ) /\ ( x e. A -> ( y = D <-> y = E ) ) ) -> A. x A. y ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) )
99 19 98 syl 
 |-  ( ( A = B /\ A. x e. A D = E ) -> A. x A. y ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) )
100 eqopab2bw 
 |-  ( { <. x , y >. | ( x e. A /\ y = D ) } = { <. x , y >. | ( x e. B /\ y = E ) } <-> A. x A. y ( ( x e. A /\ y = D ) <-> ( x e. B /\ y = E ) ) )
101 99 100 sylibr 
 |-  ( ( A = B /\ A. x e. A D = E ) -> { <. x , y >. | ( x e. A /\ y = D ) } = { <. x , y >. | ( x e. B /\ y = E ) } )
102 df-mpt 
 |-  ( x e. A |-> D ) = { <. x , y >. | ( x e. A /\ y = D ) }
103 df-mpt 
 |-  ( x e. B |-> E ) = { <. x , y >. | ( x e. B /\ y = E ) }
104 101 102 103 3eqtr4g 
 |-  ( ( A = B /\ A. x e. A D = E ) -> ( x e. A |-> D ) = ( x e. B |-> E ) )