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 37 44 47 52 4syl 
 |-  ( 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 ) ) ) )
54 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 ) ) ) ) )
55 54 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 ) ) ) ) )
56 55 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 ) ) ) ) )
57 56 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 ) ) ) ) )
58 34 53 57 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 ) ) ) ) )
59 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 ) ) )
60 59 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 ) ) )
61 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 ) ) )
62 61 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 ) ) ) )
63 60 62 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 ) ) )
64 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 ) ) ) )
65 64 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 ) ) ) )
66 65 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 ) ) ) ) )
67 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 ) ) ) ) )
68 66 67 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 ) ) )
69 68 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 ) ) ) )
70 63 69 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 ) ) )
71 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 ) )
72 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 ) ) ) )
73 72 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 ) ) ) )
74 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 ) ) ) ) ) )
75 74 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 ) ) ) ) ) ) )
76 73 75 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 ) ) ) ) ) )
77 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 ) ) ) ) )
78 77 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 ) ) ) ) ) )
79 76 78 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 ) ) ) ) )
80 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 ) ) ) ) )
81 79 80 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 ) )
82 81 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 ) ) )
83 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 ) ) )
84 83 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 ) ) ) )
85 82 84 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 ) ) )
86 71 85 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 ) )
87 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 ) ) )
88 87 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 ) ) ) )
89 86 88 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 ) ) )
90 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 ) ) )
91 90 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 ) ) ) )
92 89 91 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 ) ) )
93 70 92 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 )
94 93 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 ) )
95 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 ) ) ) ) )
96 77 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 ) ) ) ) ) )
97 95 96 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 ) ) ) ) ) )
98 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 ) ) ) ) ) )
99 98 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 ) ) ) ) ) ) )
100 97 99 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 ) ) ) ) )
101 94 100 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 ) ) ) )
102 notnotr 
 |-  ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( ( x e. B /\ y e. D ) /\ z = F ) )
103 102 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 ) ) )
104 90 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 ) ) ) )
105 103 104 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 ) ) )
106 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 ) ) )
107 106 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 ) ) ) )
108 105 107 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 ) )
109 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 ) ) ) )
110 109 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 ) ) ) )
111 74 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 ) ) ) ) ) ) )
112 110 111 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 ) ) ) ) ) )
113 77 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 ) ) ) ) ) )
114 112 113 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 ) ) ) ) )
115 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 ) ) ) ) )
116 114 115 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 ) )
117 108 116 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 ) )
118 93 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 ) )
119 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 ) ) ) ) )
120 77 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 ) ) ) ) ) )
121 119 120 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 ) ) ) ) ) )
122 98 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 ) ) ) ) ) ) )
123 121 122 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 ) ) ) ) )
124 118 123 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 ) ) ) )
125 117 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 ) -> ( z = E <-> z = F ) ) )
126 118 117 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 ) ) )
127 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 ) ) ) ) )
128 127 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 ) ) ) ) ) )
129 119 128 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 ) ) ) )
130 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 ) ) ) )
131 130 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 ) ) ) ) )
132 129 131 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 ) ) ) )
133 103 132 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 ) ) )
134 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 ) ) )
135 134 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 ) ) ) )
136 133 135 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 ) ) )
137 126 136 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 ) )
138 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 ) ) )
139 138 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 ) ) ) )
140 103 139 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 ) )
141 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 ) ) )
142 141 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 ) ) ) )
143 142 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 ) ) )
144 140 143 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 ) ) ) )
145 137 144 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 ) ) )
146 125 145 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 ) )
147 146 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 ) ) )
148 127 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 ) ) ) ) ) )
149 95 148 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 ) ) ) )
150 64 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 ) ) ) ) )
151 149 150 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 ) ) ) )
152 147 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 ) ) )
153 61 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 ) ) ) )
154 152 153 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 ) ) )
155 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 ) ) )
156 155 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 ) ) ) )
157 154 156 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 ) )
158 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 ) ) )
159 158 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 ) ) ) )
160 152 159 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 ) )
161 94 81 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 ) )
162 157 116 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 ) )
163 161 162 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 ) ) )
164 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 ) ) )
165 164 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 ) ) ) )
166 147 165 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 ) ) )
167 163 166 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 ) )
168 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 ) ) )
169 168 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 ) ) ) )
170 169 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 ) ) )
171 167 170 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 ) ) ) )
172 160 171 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 ) ) )
173 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 ) ) ) )
174 173 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 ) ) ) ) )
175 174 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 ) ) ) )
176 172 175 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 ) ) ) ) )
177 157 176 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 ) ) ) )
178 101 177 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. )
179 178 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 ) ) )
180 179 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 ) ) )
181 180 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 ) ) )
182 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 ) } )
183 58 181 182 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 ) } )
184 df-mpo 
 |-  ( x e. A , y e. C |-> E ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. C ) /\ z = E ) }
185 df-mpo 
 |-  ( x e. B , y e. D |-> F ) = { <. <. x , y >. , z >. | ( ( x e. B /\ y e. D ) /\ z = F ) }
186 183 184 185 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 ) )