Users' Mathboxes Mathbox for Giovanni Mascellani < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mpt2bi123f Structured version   Visualization version   Unicode version
Theorem mpt2bi123f 33971
Description: Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
Hypotheses
Ref Expression
mpt2bi123f.1 |- F/_ x A
mpt2bi123f.2 |- F/_ x B
mpt2bi123f.3 |- F/_ y A
mpt2bi123f.4 |- F/_ y B
mpt2bi123f.5 |- F/_ y C
mpt2bi123f.6 |- F/_ y D
mpt2bi123f.7 |- F/_ x C
mpt2bi123f.8 |- F/_ x D
Assertion
Ref Expression
mpt2bi123f |- ( ( ( 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 ) )
Distinct variable group:   x, y
Allowed substitution hints:   A( x, y)   B( x, y)   C( x, y)   D( x, y)   E( x, y)   F( x, y)
Proof of Theorem mpt2bi123f
Dummy variable z is distinct from all other variables.
StepHypRef Expression
1 mpt2bi123f.1 . . . . . . . 8 |- F/_ x A
2 mpt2bi123f.2 . . . . . . . 8 |- F/_ x B
31, 2nfeq 2776 . . . . . . 7 |- F/ x A = B
4 eleq2 2690 . . . . . . 7 |- ( A = B -> ( x e. A <-> x e. B ) )
53, 4alrimi 2082 . . . . . 6 |- ( A = B -> A. x ( x e. A <-> x e. B ) )
6 mpt2bi123f.3 . . . . . . . . . 10 |- F/_ y A
76nfcri 2758 . . . . . . . . 9 |- F/ y x e. A
8 mpt2bi123f.4 . . . . . . . . . 10 |- F/_ y B
98nfcri 2758 . . . . . . . . 9 |- F/ y x e. B
107, 9nfbi 1833 . . . . . . . 8 |- F/ y ( x e. A <-> x e. B )
11 ax-5 1839 . . . . . . . 8 |- ( ( x e. A <-> x e. B ) -> A. z ( x e. A <-> x e. B ) )
1210, 11alrimi 2082 . . . . . . 7 |- ( ( x e. A <-> x e. B ) -> A. y A. z ( x e. A <-> x e. B ) )
1312alimi 1739 . . . . . 6 |- ( A. x ( x e. A <-> x e. B ) -> A. x A. y A. z ( x e. A <-> x e. B ) )
145, 13syl 17 . . . . 5 |- ( A = B -> A. x A. y A. z ( x e. A <-> x e. B ) )
15 mpt2bi123f.5 . . . . . . . 8 |- F/_ y C
16 mpt2bi123f.6 . . . . . . . 8 |- F/_ y D
1715, 16nfeq 2776 . . . . . . 7 |- F/ y C = D
18 eleq2 2690 . . . . . . 7 |- ( C = D -> ( y e. C <-> y e. D ) )
1917, 18alrimi 2082 . . . . . 6 |- ( C = D -> A. y ( y e. C <-> y e. D ) )
20 ax-5 1839 . . . . . . 7 |- ( ( y e. C <-> y e. D ) -> A. z ( y e. C <-> y e. D ) )
2120alimi 1739 . . . . . 6 |- ( A. y ( y e. C <-> y e. D ) -> A. y A. z ( y e. C <-> y e. D ) )
22 mpt2bi123f.7 . . . . . . . . . . 11 |- F/_ x C
2322nfcri 2758 . . . . . . . . . 10 |- F/ x y e. C
24 mpt2bi123f.8 . . . . . . . . . . 11 |- F/_ x D
2524nfcri 2758 . . . . . . . . . 10 |- F/ x y e. D
2623, 25nfbi 1833 . . . . . . . . 9 |- F/ x ( y e. C <-> y e. D )
2726nfal 2153 . . . . . . . 8 |- F/ x A. z ( y e. C <-> y e. D )
2827nfal 2153 . . . . . . 7 |- F/ x A. y A. z ( y e. C <-> y e. D )
2928nf5ri 2065 . . . . . 6 |- ( A. y A. z ( y e. C <-> y e. D ) -> A. x A. y A. z ( y e. C <-> y e. D ) )
3019, 21, 293syl 18 . . . . 5 |- ( C = D -> A. x A. y A. z ( y e. C <-> y e. D ) )
31 id 22 . . . . . . . 8 |- ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) -> ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) )
3231alanimi 1744 . . . . . . 7 |- ( ( 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 ) ) )
3332alanimi 1744 . . . . . 6 |- ( ( 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 ) ) )
3433alanimi 1744 . . . . 5 |- ( ( 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 ) ) )
3514, 30, 34syl2an 494 . . . 4 |- ( ( A = B /\ C = D ) -> A. x A. y A. z ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) )
36 eqeq2 2633 . . . . . . 7 |- ( E = F -> ( z = E <-> z = F ) )
3736alrimiv 1855 . . . . . 6 |- ( E = F -> A. z ( z = E <-> z = F ) )
38372ralimi 2953 . . . . 5 |- ( A. x e. A A. y e. C E = F -> A. x e. A A. y e. C A. z ( z = E <-> z = F ) )
39 hbra1 2942 . . . . . . . . 9 |- ( A. y e. C A. z ( z = E <-> z = F ) -> A. y A. y e. C A. z ( z = E <-> z = F ) )
40 rsp 2929 . . . . . . . . 9 |- ( A. y e. C A. z ( z = E <-> z = F ) -> ( y e. C -> A. z ( z = E <-> z = F ) ) )
4139, 40alrimih 1751 . . . . . . . 8 |- ( A. y e. C A. z ( z = E <-> z = F ) -> A. y ( y e. C -> A. z ( z = E <-> z = F ) ) )
42 19.21v 1868 . . . . . . . . 9 |- ( A. z ( y e. C -> ( z = E <-> z = F ) ) <-> ( y e. C -> A. z ( z = E <-> z = F ) ) )
4342albii 1747 . . . . . . . 8 |- ( A. y A. z ( y e. C -> ( z = E <-> z = F ) ) <-> A. y ( y e. C -> A. z ( z = E <-> z = F ) ) )
4441, 43sylibr 224 . . . . . . 7 |- ( A. y e. C A. z ( z = E <-> z = F ) -> A. y A. z ( y e. C -> ( z = E <-> z = F ) ) )
4544ralimi 2952 . . . . . 6 |- ( 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 ) ) )
46 hbra1 2942 . . . . . . 7 |- ( 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 ) ) )
47 rsp 2929 . . . . . . 7 |- ( 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 ) ) ) )
4846, 47alrimih 1751 . . . . . 6 |- ( 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 ) ) ) )
49 19.21v 1868 . . . . . . . 8 |- ( A. z ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) <-> ( x e. A -> A. z ( y e. C -> ( z = E <-> z = F ) ) ) )
50492albii 1748 . . . . . . 7 |- ( 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 ) ) ) )
51719.21 2075 . . . . . . . 8 |- ( 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 ) ) ) )
5251albii 1747 . . . . . . 7 |- ( 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 ) ) ) )
5350, 52sylbbr 226 . . . . . 6 |- ( 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 ) ) ) )
5445, 48, 533syl 18 . . . . 5 |- ( 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 ) ) ) )
5538, 54syl 17 . . . 4 |- ( 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 ) ) ) )
56 id 22 . . . . . . 7 |- ( ( ( ( x 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 ) ) ) ) )
5756alanimi 1744 . . . . . 6 |- ( ( 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 ) ) ) ) )
5857alanimi 1744 . . . . 5 |- ( ( 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 ) ) ) ) )
5958alanimi 1744 . . . 4 |- ( ( 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 ) ) ) ) )
6035, 55, 59syl2an 494 . . 3 |- ( ( ( 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 ) ) ) ) )
61 tsan2 33949 . . . . . . . . . . . . 13 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
6261ord 392 . . . . . . . . . . . 12 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
63 tsan2 33949 . . . . . . . . . . . . 13 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
6463a1d 25 . . . . . . . . . . . 12 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
6562, 64cnf1dd 33892 . . . . . . . . . . 11 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
66 tsbi2 33941 . . . . . . . . . . . . . . 15 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
6766ord 392 . . . . . . . . . . . . . 14 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
6867a1dd 50 . . . . . . . . . . . . 13 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ax-1 6 . . . . . . . . . . . . 13 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) )
7068, 69contrd 33899 . . . . . . . . . . . 12 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
7170a1d 25 . . . . . . . . . . 11 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
7265, 71cnf1dd 33892 . . . . . . . . . 10 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
73 idd 24 . . . . . . . . . . . . 13 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) )
74 tsan2 33949 . . . . . . . . . . . . . . . . . . 19 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
7574ord 392 . . . . . . . . . . . . . . . . . 18 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
76 tsan2 33949 . . . . . . . . . . . . . . . . . . 19 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) ) )
7776a1d 25 . . . . . . . . . . . . . . . . . 18 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) ) ) )
7875, 77cnf1dd 33892 . . . . . . . . . . . . . . . . 17 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) ) )
79 tsim2 33938 . . . . . . . . . . . . . . . . . 18 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) )
8079a1d 25 . . . . . . . . . . . . . . . . 17 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) ) )
8178, 80cnf1dd 33892 . . . . . . . . . . . . . . . 16 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ax-1 6 . . . . . . . . . . . . . . . 16 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) )
8381, 82contrd 33899 . . . . . . . . . . . . . . 15 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) )
8483a1d 25 . . . . . . . . . . . . . 14 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
85 tsbi3 33942 . . . . . . . . . . . . . . 15 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
8685a1d 25 . . . . . . . . . . . . . 14 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
8784, 86cnfn2dd 33895 . . . . . . . . . . . . 13 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
8873, 87cnf1dd 33892 . . . . . . . . . . . 12 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) )
89 tsan2 33949 . . . . . . . . . . . . 13 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
9089a1d 25 . . . . . . . . . . . 12 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
9188, 90cnf1dd 33892 . . . . . . . . . . 11 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
92 tsan2 33949 . . . . . . . . . . . 12 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
9392a1d 25 . . . . . . . . . . 11 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
9491, 93cnf1dd 33892 . . . . . . . . . 10 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
9572, 94contrd 33899 . . . . . . . . 9 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 )
9695a1d 25 . . . . . . . 8 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) )
97 ax-1 6 . . . . . . . . . 10 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) )
9879a1d 25 . . . . . . . . . 10 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) ) )
9997, 98cnf2dd 33893 . . . . . . . . 9 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) ) )
100 tsan3 33950 . . . . . . . . . 10 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) ) )
101100a1d 25 . . . . . . . . 9 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) ) ) )
10299, 101cnfn2dd 33895 . . . . . . . 8 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) )
10396, 102mpdd 43 . . . . . . 7 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
104 notnotr 125 . . . . . . . . . . . . . . . . . 18 |- ( -. -. ( ( x e. B /\ y e. D ) /\ z = F ) -> ( ( x e. B /\ y e. D ) /\ z = F ) )
105104a1i 11 . . . . . . . . . . . . . . . . 17 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
10692a1d 25 . . . . . . . . . . . . . . . . 17 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
107105, 106cnfn2dd 33895 . . . . . . . . . . . . . . . 16 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
108 tsan3 33950 . . . . . . . . . . . . . . . . 17 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
109108a1d 25 . . . . . . . . . . . . . . . 16 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
110107, 109cnfn2dd 33895 . . . . . . . . . . . . . . 15 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) )
111 tsan3 33950 . . . . . . . . . . . . . . . . . . 19 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
112111ord 392 . . . . . . . . . . . . . . . . . 18 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
11376a1d 25 . . . . . . . . . . . . . . . . . 18 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) ) ) )
114112, 113cnf1dd 33892 . . . . . . . . . . . . . . . . 17 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) ) )
11579a1d 25 . . . . . . . . . . . . . . . . 17 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) ) )
116114, 115cnf1dd 33892 . . . . . . . . . . . . . . . 16 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ax-1 6 . . . . . . . . . . . . . . . 16 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) )
118116, 117contrd 33899 . . . . . . . . . . . . . . 15 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) )
119110, 118sylibrd 249 . . . . . . . . . . . . . 14 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) )
12095a1d 25 . . . . . . . . . . . . . . 15 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) )
121 ax-1 6 . . . . . . . . . . . . . . . . 17 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) )
12279a1d 25 . . . . . . . . . . . . . . . . 17 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) ) )
123121, 122cnf2dd 33893 . . . . . . . . . . . . . . . 16 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) ) )
124100a1d 25 . . . . . . . . . . . . . . . 16 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) ) ) )
125123, 124cnfn2dd 33895 . . . . . . . . . . . . . . 15 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) )
126120, 125mpdd 43 . . . . . . . . . . . . . 14 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
127119, 126mpdd 43 . . . . . . . . . . . . 13 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
128120, 119jcad 555 . . . . . . . . . . . . . . 15 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
129 tsim3 33939 . . . . . . . . . . . . . . . . . . . 20 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) )
130129a1d 25 . . . . . . . . . . . . . . . . . . 19 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) ) )
131121, 130cnf2dd 33893 . . . . . . . . . . . . . . . . . 18 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
132 tsbi1 33940 . . . . . . . . . . . . . . . . . . 19 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
133132a1d 25 . . . . . . . . . . . . . . . . . 18 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) )
134131, 133cnf2dd 33893 . . . . . . . . . . . . . . . . 17 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
135105, 134cnfn2dd 33895 . . . . . . . . . . . . . . . 16 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
136 tsan1 33948 . . . . . . . . . . . . . . . . 17 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
137136a1d 25 . . . . . . . . . . . . . . . 16 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
138135, 137cnf2dd 33893 . . . . . . . . . . . . . . 15 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
139128, 138cnfn1dd 33894 . . . . . . . . . . . . . 14 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) )
140 tsan3 33950 . . . . . . . . . . . . . . . . 17 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
141140a1d 25 . . . . . . . . . . . . . . . 16 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
142105, 141cnfn2dd 33895 . . . . . . . . . . . . . . 15 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) )
143 tsbi3 33942 . . . . . . . . . . . . . . . . 17 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
144143a1d 25 . . . . . . . . . . . . . . . 16 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
145144or32dd 33896 . . . . . . . . . . . . . . 15 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
146142, 145cnfn2dd 33895 . . . . . . . . . . . . . 14 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
147139, 146cnf1dd 33892 . . . . . . . . . . . . 13 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
148127, 147contrd 33899 . . . . . . . . . . . 12 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) )
149148a1d 25 . . . . . . . . . . 11 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
150129a1d 25 . . . . . . . . . . . . 13 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) ) )
15197, 150cnf2dd 33893 . . . . . . . . . . . 12 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
15266a1d 25 . . . . . . . . . . . 12 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) )
153151, 152cnf2dd 33893 . . . . . . . . . . 11 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
154149, 153cnf2dd 33893 . . . . . . . . . 10 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
15563a1d 25 . . . . . . . . . 10 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
156154, 155cnfn2dd 33895 . . . . . . . . 9 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
157 tsan3 33950 . . . . . . . . . 10 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
158157a1d 25 . . . . . . . . 9 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
159156, 158cnfn2dd 33895 . . . . . . . 8 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) )
160 tsan3 33950 . . . . . . . . . . . 12 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
161160a1d 25 . . . . . . . . . . 11 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
162154, 161cnfn2dd 33895 . . . . . . . . . 10 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) )
16396, 83sylibd 229 . . . . . . . . . . . . 13 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) )
164159, 118sylibd 229 . . . . . . . . . . . . 13 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) )
165163, 164jcad 555 . . . . . . . . . . . 12 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
166 tsan1 33948 . . . . . . . . . . . . . 14 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
167166a1d 25 . . . . . . . . . . . . 13 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
168149, 167cnf2dd 33893 . . . . . . . . . . . 12 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
169165, 168cnfn1dd 33894 . . . . . . . . . . 11 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) )
170 tsbi4 33943 . . . . . . . . . . . . 13 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
171170a1d 25 . . . . . . . . . . . 12 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
172171or32dd 33896 . . . . . . . . . . 11 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
173169, 172cnf2dd 33893 . . . . . . . . . 10 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
174162, 173cnfn1dd 33894 . . . . . . . . 9 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) )
175 tsim1 33937 . . . . . . . . . . 11 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
176175a1d 25 . . . . . . . . . 10 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) )
177176or32dd 33896 . . . . . . . . 9 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
178174, 177cnf2dd 33893 . . . . . . . 8 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) ) )
179159, 178cnfn1dd 33894 . . . . . . 7 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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 ) ) ) )
180103, 179contrd 33899 . . . . . 6 |- ( -. ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. 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. )
181180efald2 33877 . . . . 5 |- ( ( ( ( x e. A <-> x e. B ) /\ ( y e. C <-> y e. D ) ) /\ ( x e. A -> ( y e. C -> ( z = E <-> z = F ) ) ) ) -> ( ( ( x e. A /\ y e. C ) /\ z = E ) <-> ( ( x e. B /\ y e. D ) /\ z = F ) ) )
182181alimi 1739 . . . 4 |- ( 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 ) ) )
1831822alimi 1740 . . 3 |- ( 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 ) ) )
184 oprabbi 33970 . . 3 |- ( 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 ) } )
18560, 183, 1843syl 18 . 2 |- ( ( ( 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 ) } )
186 df-mpt2 6655 . 2 |- ( x e. A , y e. C |-> E ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. C ) /\ z = E ) }
187 df-mpt2 6655 . 2 |- ( x e. B , y e. D |-> F ) = { <. <. x , y >. , z >. | ( ( x e. B /\ y e. D ) /\ z = F ) }
188185, 186, 1873eqtr4g 2681 1 |- ( ( ( 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 ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   A.wal 1481   = wceq 1483   F. wfal 1488   e. wcel 1990   F/_wnfc 2751   A.wral 2912   {coprab 6651   |-> cmpt2 6652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-oprab 6654  df-mpt2 6655
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator