Metamath Proof Explorer

Theorem mpobi123f

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

Ref Expression
Hypotheses mpobi123f.1 
|- F/_ x A
mpobi123f.2 
|- F/_ x B
mpobi123f.3 
|- F/_ y A
mpobi123f.4 
|- F/_ y B
mpobi123f.5 
|- F/_ y C
mpobi123f.6 
|- F/_ y D
mpobi123f.7 
|- F/_ x C
mpobi123f.8 
|- F/_ x D
Assertion mpobi123f 
|- ( ( ( A = B /\ C = D ) /\ A. x e. A A. y e. C E = F ) -> ( x e. A , y e. C |-> E ) = ( x e. B , y e. D |-> F ) )

Proof

Step Hyp Ref Expression
1 mpobi123f.1 
 |-  F/_ x A
2 mpobi123f.2 
 |-  F/_ x B
3 mpobi123f.3 
 |-  F/_ y A
4 mpobi123f.4 
 |-  F/_ y B
5 mpobi123f.5 
 |-  F/_ y C
6 mpobi123f.6 
 |-  F/_ y D
7 mpobi123f.7 
 |-  F/_ x C
8 mpobi123f.8 
 |-  F/_ x D
9 1 2 nfeq 
 |-  F/ x A = B
10 eleq2 
 |-  ( A = B -> ( x e. A <-> x e. B ) )
11 9 10 alrimi 
 |-  ( A = B -> A. x ( x e. A <-> x e. B ) )
12 3 nfcri 
 |-  F/ y x e. A
13 4 nfcri 
 |-  F/ y x e. B
14 12 13 nfbi 
 |-  F/ y ( x e. A <-> x e. B )
15 ax-5 
 |-  ( ( x e. A <-> x e. B ) -> A. z ( x e. A <-> x e. B ) )
16 14 15 alrimi 
 |-  ( ( x e. A <-> x e. B ) -> A. y A. z ( x e. A <-> x e. B ) )
17 11 16 sylg 
 |-  ( A = B -> A. x A. y A. z ( x e. A <-> x e. B ) )
18 5 6 nfeq 
 |-  F/ y C = D
19 eleq2 
 |-  ( C = D -> ( y e. C <-> y e. D ) )
20 18 19 alrimi 
 |-  ( C = D -> A. y ( y e. C <-> y e. D ) )
21 ax-5 
 |-  ( ( y e. C <-> y e. D ) -> A. z ( y e. C <-> y e. D ) )
22 21 alimi 
 |-  ( A. y ( y e. C <-> y e. D ) -> A. y A. z ( y e. C <-> y e. D ) )
23 7 nfcri 
 |-  F/ x y e. C
24 8 nfcri 
 |-  F/ x y e. D
25 23 24 nfbi 
 |-  F/ x ( y e. C <-> y e. D )
26 25 nfal 
 |-  F/ x A. z ( y e. C <-> y e. D )
27 26 nfal 
 |-  F/ x A. y A. z ( y e. C <-> y e. D )
28 27 nf5ri 
 |-  ( A. y A. z ( y e. C <-> y e. D ) -> A. x A. y A. z ( y e. C <-> y e. D ) )
29 20 22 28 3syl 
 |-  ( C = D -> A. x A. y A. z ( y e. C <-> y e. D ) )
30 id 
 |-  ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) -> ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) )
31 30 alanimi 
 |-  ( ( A. z ( x e. A <-> x e. B ) /\ A. z ( y e. C <-> y e. D ) ) -> A. z ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) )
32 31 alanimi 
 |-  ( ( A. y A. z ( x e. A <-> x e. B ) /\ A. y A. z ( y e. C <-> y e. D ) ) -> A. y A. z ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) )
33 32 alanimi 
 |-  ( ( A. x A. y A. z ( x e. A <-> x e. B ) /\ A. x A. y A. z ( y e. C <-> y e. D ) ) -> A. x A. y A. z ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) )
34 17 29 33 syl2an 
 |-  ( ( A = B /\ C = D ) -> A. x A. y A. z ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) )
35 eqeq2 
 |-  ( E = F -> ( z = E <-> z = F ) )
36 35 alrimiv 
 |-  ( E = F -> A. z ( z = E <-> z = F ) )
37 36 2ralimi 
 |-  ( A. x e. A A. y e. C E = F -> A. x e. A A. y e. C A. z ( z = E <-> z = F ) )
38 hbra1 
 |-  ( A. y e. C A. z ( z = E <-> z = F ) -> A. y A. y e. C A. z ( z = E <-> z = F ) )
39 rsp 
 |-  ( A. y e. C A. z ( z = E <-> z = F ) -> ( y e. C -> A. z ( z = E <-> z = F ) ) )
40 38 39 alrimih 
 |-  ( A. y e. C A. z ( z = E <-> z = F ) -> A. y ( y e. C -> A. z ( z = E <-> z = F ) ) )
41 19.21v 
 |-  ( A. z ( y e. C -> ( z = E <-> z = F ) ) <-> ( y e. C -> A. z ( z = E <-> z = F ) ) )
42 41 albii 
 |-  ( A. y A. z ( y e. C -> ( z = E <-> z = F ) ) <-> A. y ( y e. C -> A. z ( z = E <-> z = F ) ) )
43 40 42 sylibr 
 |-  ( A. y e. C A. z ( z = E <-> z = F ) -> A. y A. z ( y e. C -> ( z = E <-> z = F ) ) )
44 43 ralimi 
 |-  ( A. x e. A A. y e. C A. z ( z = E <-> z = F ) -> A. x e. A A. y A. z ( y e. C -> ( z = E <-> z = F ) ) )
45 hbra1 
 |-  ( A. x e. A A. y A. z ( y e. C -> ( z = E <-> z = F ) ) -> A. x A. x e. A A. y A. z ( y e. C -> ( z = E <-> z = F ) ) )
46 rsp 
 |-  ( A. x e. A A. y A. z ( y e. C -> ( z = E <-> z = F ) ) -> ( x e. A -> A. y A. z ( y e. C -> ( z = E <-> z = F ) ) ) )
47 45 46 alrimih 
 |-  ( A. x e. A A. y A. z ( y e. C -> ( z = E <-> z = F ) ) -> A. x ( x e. A -> A. y A. z ( y e. C -> ( z = E <-> z = F ) ) ) )
48 19.21v 
 |-  ( A. z ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) <-> ( x e. A -> A. z ( y e. C -> ( z = E <-> z = F ) ) ) )
49 48 2albii 
 |-  ( A. x A. y A. z ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) <-> A. x A. y ( x e. A -> A. z ( y e. C -> ( z = E <-> z = F ) ) ) )
50 12 19.21 
 |-  ( A. y ( x e. A -> A. z ( y e. C -> ( z = E <-> z = F ) ) ) <-> ( x e. A -> A. y A. z ( y e. C -> ( z = E <-> z = F ) ) ) )
51 50 albii 
 |-  ( A. x A. y ( x e. A -> A. z ( y e. C -> ( z = E <-> z = F ) ) ) <-> A. x ( x e. A -> A. y A. z ( y e. C -> ( z = E <-> z = F ) ) ) )
52 49 51 sylbbr 
 |-  ( A. x ( x e. A -> A. y A. z ( y e. C -> ( z = E <-> z = F ) ) ) -> A. x A. y A. z ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) )
53 44 47 52 3syl 
 |-  ( A. x e. A A. y e. C A. z ( z = E <-> z = F ) -> A. x A. y A. z ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) )
54 37 53 syl 
 |-  ( A. x e. A A. y e. C E = F -> A. x A. y A. z ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) )
55 id 
 |-  ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) )
56 55 alanimi 
 |-  ( ( A. z ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ A. z ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> A. z ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) )
57 56 alanimi 
 |-  ( ( A. y A. z ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ A. y A. z ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> A. y A. z ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) )
58 57 alanimi 
 |-  ( ( A. x A. y A. z ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ A. x A. y A. z ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> A. x A. y A. z ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) )
59 34 54 58 syl2an 
 |-  ( ( ( A = B /\ C = D ) /\ A. x e. A A. y e. C E = F ) -> A. x A. y A. z ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) )
60 tsan2 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( x e. A \/ -. ( x e. A /\ y e. C ) ) )
61 60 ord 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. x e. A -> -. ( x e. A /\ y e. C ) ) )
62 tsan2 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( ( x e. A /\ y e. C ) \/ -. ( ( x e. A /\ y e. C ) /\ z = E ) ) )
63 62 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. x e. A -> ( ( x e. A /\ y e. C ) \/ -. ( ( x e. A /\ y e. C ) /\ z = E ) ) ) )
64 61 63 cnf1dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. x e. A -> -. ( ( x e. A /\ y e. C ) /\ z = E ) ) )
65 tsbi2 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( ( ( ( x e. A /\ y e. C ) /\ z = E ) \/ ( ( x e. B /\ y e. D ) /\ z = F ) ) \/ ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) )
66 65 ord 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. ( ( ( x e. A /\ y e. C ) /\ z = E ) \/ ( ( x e. B /\ y e. D ) /\ z = F ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) )
67 66 a1dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. ( ( ( x e. A /\ y e. C ) /\ z = E ) \/ ( ( x e. B /\ y e. D ) /\ z = F ) ) -> ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) )
68 ax-1 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. ( ( ( x e. A /\ y e. C ) /\ z = E ) \/ ( ( x e. B /\ y e. D ) /\ z = F ) ) -> -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) )
69 67 68 contrd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) \/ ( ( x e. B /\ y e. D ) /\ z = F ) ) )
70 69 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. x e. A -> ( ( ( x e. A /\ y e. C ) /\ z = E ) \/ ( ( x e. B /\ y e. D ) /\ z = F ) ) ) )
71 64 70 cnf1dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. x e. A -> ( ( x e. B /\ y e. D ) /\ z = F ) ) )
72 idd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. x e. A -> -. x e. A ) )
73 tsan2 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( ( x e. A <-> x e. B ) \/ -. ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) ) )
74 73 ord 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. ( x e. A <-> x e. B ) -> -. ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) ) )
75 tsan2 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) \/ -. ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) ) )
76 75 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. ( x e. A <-> x e. B ) -> ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) \/ -. ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) ) ) )
77 74 76 cnf1dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. ( x e. A <-> x e. B ) -> -. ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) ) )
78 tsim2 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) \/ ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) )
79 78 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. ( x e. A <-> x e. B ) -> ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) \/ ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) ) )
80 77 79 cnf1dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. ( x e. A <-> x e. B ) -> ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) )
81 ax-1 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. ( x e. A <-> x e. B ) -> -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) )
82 80 81 contrd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( x e. A <-> x e. B ) )
83 82 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. x e. A -> ( x e. A <-> x e. B ) ) )
84 tsbi3 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( ( x e. A \/ -. x e. B ) \/ -. ( x e. A <-> x e. B ) ) )
85 84 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. x e. A -> ( ( x e. A \/ -. x e. B ) \/ -. ( x e. A <-> x e. B ) ) ) )
86 83 85 cnfn2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. x e. A -> ( x e. A \/ -. x e. B ) ) )
87 72 86 cnf1dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. x e. A -> -. x e. B ) )
88 tsan2 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( x e. B \/ -. ( x e. B /\ y e. D ) ) )
89 88 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. x e. A -> ( x e. B \/ -. ( x e. B /\ y e. D ) ) ) )
90 87 89 cnf1dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. x e. A -> -. ( x e. B /\ y e. D ) ) )
91 tsan2 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( ( x e. B /\ y e. D ) \/ -. ( ( x e. B /\ y e. D ) /\ z = F ) ) )
92 91 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. x e. A -> ( ( x e. B /\ y e. D ) \/ -. ( ( x e. B /\ y e. D ) /\ z = F ) ) ) )
93 90 92 cnf1dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. x e. A -> -. ( ( x e. B /\ y e. D ) /\ z = F ) ) )
94 71 93 contrd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> x e. A )
95 94 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> x e. A ) )
96 ax-1 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) )
97 78 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) \/ ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) ) )
98 96 97 cnf2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) ) )
99 tsan3 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) \/ -. ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) ) )
100 99 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) \/ -. ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) ) ) )
101 98 100 cnfn2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) )
102 95 101 mpdd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( y e. C -> ( z = E <-> z = F ) ) ) )
103 notnotr 
 |-  ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( ( x e. B /\ y e. D ) /\ z = F ) )
104 103 a1i 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( ( x e. B /\ y e. D ) /\ z = F ) ) )
105 91 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( ( x e. B /\ y e. D ) \/ -. ( ( x e. B /\ y e. D ) /\ z = F ) ) ) )
106 104 105 cnfn2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( x e. B /\ y e. D ) ) )
107 tsan3 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( y e. D \/ -. ( x e. B /\ y e. D ) ) )
108 107 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( y e. D \/ -. ( x e. B /\ y e. D ) ) ) )
109 106 108 cnfn2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> y e. D ) )
110 tsan3 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( ( y e. C <-> y e. D ) \/ -. ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) ) )
111 110 ord 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. ( y e. C <-> y e. D ) -> -. ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) ) )
112 75 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. ( y e. C <-> y e. D ) -> ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) \/ -. ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) ) ) )
113 111 112 cnf1dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. ( y e. C <-> y e. D ) -> -. ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) ) )
114 78 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. ( y e. C <-> y e. D ) -> ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) \/ ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) ) )
115 113 114 cnf1dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. ( y e. C <-> y e. D ) -> ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) )
116 ax-1 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. ( y e. C <-> y e. D ) -> -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) )
117 115 116 contrd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( y e. C <-> y e. D ) )
118 109 117 sylibrd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> y e. C ) )
119 94 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> x e. A ) )
120 ax-1 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) )
121 78 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) \/ ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) ) )
122 120 121 cnf2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) ) )
123 99 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) \/ -. ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) ) ) )
124 122 123 cnfn2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) )
125 119 124 mpdd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( y e. C -> ( z = E <-> z = F ) ) ) )
126 118 125 mpdd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( z = E <-> z = F ) ) )
127 119 118 jcad 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( x e. A /\ y e. C ) ) )
128 tsim3 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) \/ ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) )
129 128 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( -. ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) \/ ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) ) )
130 120 129 cnf2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> -. ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) )
131 tsbi1 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( ( -. ( ( x e. A /\ y e. C ) /\ z = E ) \/ -. ( ( x e. B /\ y e. D ) /\ z = F ) ) \/ ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) )
132 131 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( ( -. ( ( x e. A /\ y e. C ) /\ z = E ) \/ -. ( ( x e. B /\ y e. D ) /\ z = F ) ) \/ ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) )
133 130 132 cnf2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( -. ( ( x e. A /\ y e. C ) /\ z = E ) \/ -. ( ( x e. B /\ y e. D ) /\ z = F ) ) ) )
134 104 133 cnfn2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> -. ( ( x e. A /\ y e. C ) /\ z = E ) ) )
135 tsan1 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( ( -. ( x e. A /\ y e. C ) \/ -. z = E ) \/ ( ( x e. A /\ y e. C ) /\ z = E ) ) )
136 135 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( ( -. ( x e. A /\ y e. C ) \/ -. z = E ) \/ ( ( x e. A /\ y e. C ) /\ z = E ) ) ) )
137 134 136 cnf2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( -. ( x e. A /\ y e. C ) \/ -. z = E ) ) )
138 127 137 cnfn1dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> -. z = E ) )
139 tsan3 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( z = F \/ -. ( ( x e. B /\ y e. D ) /\ z = F ) ) )
140 139 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( z = F \/ -. ( ( x e. B /\ y e. D ) /\ z = F ) ) ) )
141 104 140 cnfn2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> z = F ) )
142 tsbi3 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( ( z = E \/ -. z = F ) \/ -. ( z = E <-> z = F ) ) )
143 142 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( ( z = E \/ -. z = F ) \/ -. ( z = E <-> z = F ) ) ) )
144 143 or32dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( ( z = E \/ -. ( z = E <-> z = F ) ) \/ -. z = F ) ) )
145 141 144 cnfn2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( z = E \/ -. ( z = E <-> z = F ) ) ) )
146 138 145 cnf1dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> -. ( z = E <-> z = F ) ) )
147 126 146 contrd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> -. ( ( x e. B /\ y e. D ) /\ z = F ) )
148 147 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> -. ( ( x e. B /\ y e. D ) /\ z = F ) ) )
149 128 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( -. ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) \/ ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) ) )
150 96 149 cnf2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> -. ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) )
151 65 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( ( ( ( x e. A /\ y e. C ) /\ z = E ) \/ ( ( x e. B /\ y e. D ) /\ z = F ) ) \/ ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) ) )
152 150 151 cnf2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( ( ( x e. A /\ y e. C ) /\ z = E ) \/ ( ( x e. B /\ y e. D ) /\ z = F ) ) ) )
153 148 152 cnf2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( ( x e. A /\ y e. C ) /\ z = E ) ) )
154 62 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( ( x e. A /\ y e. C ) \/ -. ( ( x e. A /\ y e. C ) /\ z = E ) ) ) )
155 153 154 cnfn2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( x e. A /\ y e. C ) ) )
156 tsan3 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( y e. C \/ -. ( x e. A /\ y e. C ) ) )
157 156 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( y e. C \/ -. ( x e. A /\ y e. C ) ) ) )
158 155 157 cnfn2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> y e. C ) )
159 tsan3 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( z = E \/ -. ( ( x e. A /\ y e. C ) /\ z = E ) ) )
160 159 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( z = E \/ -. ( ( x e. A /\ y e. C ) /\ z = E ) ) ) )
161 153 160 cnfn2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> z = E ) )
162 95 82 sylibd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> x e. B ) )
163 158 117 sylibd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> y e. D ) )
164 162 163 jcad 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( x e. B /\ y e. D ) ) )
165 tsan1 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( ( -. ( x e. B /\ y e. D ) \/ -. z = F ) \/ ( ( x e. B /\ y e. D ) /\ z = F ) ) )
166 165 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( ( -. ( x e. B /\ y e. D ) \/ -. z = F ) \/ ( ( x e. B /\ y e. D ) /\ z = F ) ) ) )
167 148 166 cnf2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( -. ( x e. B /\ y e. D ) \/ -. z = F ) ) )
168 164 167 cnfn1dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> -. z = F ) )
169 tsbi4 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( ( -. z = E \/ z = F ) \/ -. ( z = E <-> z = F ) ) )
170 169 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( ( -. z = E \/ z = F ) \/ -. ( z = E <-> z = F ) ) ) )
171 170 or32dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( ( -. z = E \/ -. ( z = E <-> z = F ) ) \/ z = F ) ) )
172 168 171 cnf2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( -. z = E \/ -. ( z = E <-> z = F ) ) ) )
173 161 172 cnfn1dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> -. ( z = E <-> z = F ) ) )
174 tsim1 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( ( -. y e. C \/ ( z = E <-> z = F ) ) \/ -. ( y e. C -> ( z = E <-> z = F ) ) ) )
175 174 a1d 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( ( -. y e. C \/ ( z = E <-> z = F ) ) \/ -. ( y e. C -> ( z = E <-> z = F ) ) ) ) )
176 175 or32dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( ( -. y e. C \/ -. ( y e. C -> ( z = E <-> z = F ) ) ) \/ ( z = E <-> z = F ) ) ) )
177 173 176 cnf2dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> ( -. y e. C \/ -. ( y e. C -> ( z = E <-> z = F ) ) ) ) )
178 158 177 cnfn1dd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> ( -. F. -> -. ( y e. C -> ( z = E <-> z = F ) ) ) )
179 102 178 contrd 
 |-  ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) ) -> F. )
180 179 efald2 
 |-  ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) )
181 180 alimi 
 |-  ( A. z ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> A. z ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) )
182 181 2alimi 
 |-  ( A. x A. y A. z ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> A. x A. y A. z ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) )
183 oprabbi 
 |-  ( A. x A. y A. z ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) -> { <. <. x , y >. , z >. | ( ( x e. A /\ y e. C ) /\ z = E ) } = { <. <. x , y >. , z >. | ( ( x e. B /\ y e. D ) /\ z = F ) } )
184 59 182 183 3syl 
 |-  ( ( ( A = B /\ C = D ) /\ A. x e. A A. y e. C E = F ) -> { <. <. x , y >. , z >. | ( ( x e. A /\ y e. C ) /\ z = E ) } = { <. <. x , y >. , z >. | ( ( x e. B /\ y e. D ) /\ z = F ) } )
185 df-mpo 
 |-  ( x e. A , y e. C |-> E ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. C ) /\ z = E ) }
186 df-mpo 
 |-  ( x e. B , y e. D |-> F ) = { <. <. x , y >. , z >. | ( ( x e. B /\ y e. D ) /\ z = F ) }
187 184 185 186 3eqtr4g 
 |-  ( ( ( A = B /\ C = D ) /\ A. x e. A A. y e. C E = F ) -> ( x e. A , y e. C |-> E ) = ( x e. B , y e. D |-> F ) )