Users' Mathboxes Mathbox for Giovanni Mascellani < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mptbi12f Structured version   Visualization version   GIF version
Theorem mptbi12f 37022
Description: Equality deduction for maps-to notations. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
Hypotheses
Ref Expression
mptbi12f.1 β„²π‘₯𝐴
mptbi12f.2 β„²π‘₯𝐡
Assertion
Ref Expression
mptbi12f ((𝐴 = 𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 𝐷 = 𝐸) β†’ (π‘₯ ∈ 𝐴 ↦ 𝐷) = (π‘₯ ∈ 𝐡 ↦ 𝐸))
Proof of Theorem mptbi12f
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 mptbi12f.1 . . . . . . . 8 β„²π‘₯𝐴
2 mptbi12f.2 . . . . . . . 8 β„²π‘₯𝐡
31, 2nfeq 2916 . . . . . . 7 β„²π‘₯ 𝐴 = 𝐡
4 eleq2 2822 . . . . . . 7 (𝐴 = 𝐡 β†’ (π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡))
53, 4alrimi 2206 . . . . . 6 (𝐴 = 𝐡 β†’ βˆ€π‘₯(π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡))
6 ax-5 1913 . . . . . 6 ((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) β†’ βˆ€π‘¦(π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡))
75, 6sylg 1825 . . . . 5 (𝐴 = 𝐡 β†’ βˆ€π‘₯βˆ€π‘¦(π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡))
8 eqeq2 2744 . . . . . . . . 9 (𝐷 = 𝐸 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))
98alrimiv 1930 . . . . . . . 8 (𝐷 = 𝐸 β†’ βˆ€π‘¦(𝑦 = 𝐷 ↔ 𝑦 = 𝐸))
109ralimi 3083 . . . . . . 7 (βˆ€π‘₯ ∈ 𝐴 𝐷 = 𝐸 β†’ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦(𝑦 = 𝐷 ↔ 𝑦 = 𝐸))
11 df-ral 3062 . . . . . . 7 (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦(𝑦 = 𝐷 ↔ 𝑦 = 𝐸) ↔ βˆ€π‘₯(π‘₯ ∈ 𝐴 β†’ βˆ€π‘¦(𝑦 = 𝐷 ↔ 𝑦 = 𝐸)))
1210, 11sylib 217 . . . . . 6 (βˆ€π‘₯ ∈ 𝐴 𝐷 = 𝐸 β†’ βˆ€π‘₯(π‘₯ ∈ 𝐴 β†’ βˆ€π‘¦(𝑦 = 𝐷 ↔ 𝑦 = 𝐸)))
13 19.21v 1942 . . . . . . 7 (βˆ€π‘¦(π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)) ↔ (π‘₯ ∈ 𝐴 β†’ βˆ€π‘¦(𝑦 = 𝐷 ↔ 𝑦 = 𝐸)))
1413albii 1821 . . . . . 6 (βˆ€π‘₯βˆ€π‘¦(π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)) ↔ βˆ€π‘₯(π‘₯ ∈ 𝐴 β†’ βˆ€π‘¦(𝑦 = 𝐷 ↔ 𝑦 = 𝐸)))
1512, 14sylibr 233 . . . . 5 (βˆ€π‘₯ ∈ 𝐴 𝐷 = 𝐸 β†’ βˆ€π‘₯βˆ€π‘¦(π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)))
16 id 22 . . . . . . 7 (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))))
1716alanimi 1818 . . . . . 6 ((βˆ€π‘¦(π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ βˆ€π‘¦(π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ βˆ€π‘¦((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))))
1817alanimi 1818 . . . . 5 ((βˆ€π‘₯βˆ€π‘¦(π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ βˆ€π‘₯βˆ€π‘¦((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))))
197, 15, 18syl2an 596 . . . 4 ((𝐴 = 𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 𝐷 = 𝐸) β†’ βˆ€π‘₯βˆ€π‘¦((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))))
20 tsan2 36998 . . . . . . . . . . . 12 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (π‘₯ ∈ 𝐴 ∨ Β¬ (π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷)))
2120ord 862 . . . . . . . . . . 11 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ π‘₯ ∈ 𝐴 β†’ Β¬ (π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷)))
22 tsbi2 36990 . . . . . . . . . . . . . . 15 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ∨ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)) ∨ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))))
2322ord 862 . . . . . . . . . . . . . 14 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ∨ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))))
2423a1dd 50 . . . . . . . . . . . . 13 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ∨ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)) β†’ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)))))
25 ax-1 6 . . . . . . . . . . . . 13 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ∨ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)) β†’ Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)))))
2624, 25contrd 36953 . . . . . . . . . . . 12 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ∨ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)))
2726a1d 25 . . . . . . . . . . 11 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ π‘₯ ∈ 𝐴 β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ∨ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))))
2821, 27cnf1dd 36946 . . . . . . . . . 10 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ π‘₯ ∈ 𝐴 β†’ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)))
29 simplim 167 . . . . . . . . . . . . . 14 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))))
3029a1d 25 . . . . . . . . . . . . 13 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ (π‘₯ ∈ 𝐴 ∨ Β¬ π‘₯ ∈ 𝐡) β†’ ((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)))))
31 tsbi3 36991 . . . . . . . . . . . . . . 15 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∨ Β¬ π‘₯ ∈ 𝐡) ∨ Β¬ (π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡)))
3231ord 862 . . . . . . . . . . . . . 14 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ (π‘₯ ∈ 𝐴 ∨ Β¬ π‘₯ ∈ 𝐡) β†’ Β¬ (π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡)))
33 tsan2 36998 . . . . . . . . . . . . . . 15 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∨ Β¬ ((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)))))
3433a1d 25 . . . . . . . . . . . . . 14 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ (π‘₯ ∈ 𝐴 ∨ Β¬ π‘₯ ∈ 𝐡) β†’ ((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∨ Β¬ ((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))))))
3532, 34cnf1dd 36946 . . . . . . . . . . . . 13 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ (π‘₯ ∈ 𝐴 ∨ Β¬ π‘₯ ∈ 𝐡) β†’ Β¬ ((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)))))
3630, 35contrd 36953 . . . . . . . . . . . 12 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (π‘₯ ∈ 𝐴 ∨ Β¬ π‘₯ ∈ 𝐡))
3736ord 862 . . . . . . . . . . 11 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ π‘₯ ∈ 𝐴 β†’ Β¬ π‘₯ ∈ 𝐡))
38 tsan2 36998 . . . . . . . . . . . 12 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (π‘₯ ∈ 𝐡 ∨ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)))
3938a1d 25 . . . . . . . . . . 11 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ π‘₯ ∈ 𝐴 β†’ (π‘₯ ∈ 𝐡 ∨ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))))
4037, 39cnf1dd 36946 . . . . . . . . . 10 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ π‘₯ ∈ 𝐴 β†’ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)))
4128, 40contrd 36953 . . . . . . . . 9 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ π‘₯ ∈ 𝐴)
4241a1d 25 . . . . . . . 8 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ π‘₯ ∈ 𝐴))
4329a1d 25 . . . . . . . . 9 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ ((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)))))
44 tsan3 36999 . . . . . . . . . 10 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)) ∨ Β¬ ((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)))))
4544a1d 25 . . . . . . . . 9 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ ((π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)) ∨ Β¬ ((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))))))
4643, 45cnfn2dd 36949 . . . . . . . 8 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))))
4742, 46mpdd 43 . . . . . . 7 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)))
48 notnotr 130 . . . . . . . . . . . . . . . 16 (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))
4948a1i 11 . . . . . . . . . . . . . . 15 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)))
5038a1d 25 . . . . . . . . . . . . . . 15 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ (π‘₯ ∈ 𝐡 ∨ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))))
5149, 50cnfn2dd 36949 . . . . . . . . . . . . . 14 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ π‘₯ ∈ 𝐡))
5236a1d 25 . . . . . . . . . . . . . 14 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ (π‘₯ ∈ 𝐴 ∨ Β¬ π‘₯ ∈ 𝐡)))
5351, 52cnfn2dd 36949 . . . . . . . . . . . . 13 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ π‘₯ ∈ 𝐴))
54 tsan3 36999 . . . . . . . . . . . . . . . 16 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (𝑦 = 𝐸 ∨ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)))
5554a1d 25 . . . . . . . . . . . . . . 15 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ (𝑦 = 𝐸 ∨ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))))
5649, 55cnfn2dd 36949 . . . . . . . . . . . . . 14 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ 𝑦 = 𝐸))
5729a1d 25 . . . . . . . . . . . . . . . . 17 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ ((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)))))
5844a1d 25 . . . . . . . . . . . . . . . . 17 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ ((π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)) ∨ Β¬ ((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))))))
5957, 58cnfn2dd 36949 . . . . . . . . . . . . . . . 16 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))))
6053, 59mpdd 43 . . . . . . . . . . . . . . 15 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)))
61 tsbi3 36991 . . . . . . . . . . . . . . . 16 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ ((𝑦 = 𝐷 ∨ Β¬ 𝑦 = 𝐸) ∨ Β¬ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)))
6261a1d 25 . . . . . . . . . . . . . . 15 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ ((𝑦 = 𝐷 ∨ Β¬ 𝑦 = 𝐸) ∨ Β¬ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))))
6360, 62cnfn2dd 36949 . . . . . . . . . . . . . 14 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ (𝑦 = 𝐷 ∨ Β¬ 𝑦 = 𝐸)))
6456, 63cnfn2dd 36949 . . . . . . . . . . . . 13 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ 𝑦 = 𝐷))
6553, 64jcad 513 . . . . . . . . . . . 12 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ (π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷)))
66 ax-1 6 . . . . . . . . . . . . . . 15 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)))))
67 tsim3 36988 . . . . . . . . . . . . . . . 16 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)) ∨ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)))))
6867a1d 25 . . . . . . . . . . . . . . 15 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ (Β¬ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)) ∨ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))))))
6966, 68cnf2dd 36947 . . . . . . . . . . . . . 14 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ Β¬ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))))
70 tsbi1 36989 . . . . . . . . . . . . . . 15 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ ((Β¬ (π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ∨ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)) ∨ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))))
7170a1d 25 . . . . . . . . . . . . . 14 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ ((Β¬ (π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ∨ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)) ∨ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)))))
7269, 71cnf2dd 36947 . . . . . . . . . . . . 13 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ (Β¬ (π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ∨ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))))
7349, 72cnfn2dd 36949 . . . . . . . . . . . 12 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸) β†’ Β¬ (π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷)))
7465, 73contrd 36953 . . . . . . . . . . 11 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))
7574a1d 25 . . . . . . . . . 10 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ Β¬ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)))
7626a1d 25 . . . . . . . . . 10 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ∨ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))))
7775, 76cnf2dd 36947 . . . . . . . . 9 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ (π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷)))
78 tsan3 36999 . . . . . . . . . 10 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (𝑦 = 𝐷 ∨ Β¬ (π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷)))
7978a1d 25 . . . . . . . . 9 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ (𝑦 = 𝐷 ∨ Β¬ (π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷))))
8077, 79cnfn2dd 36949 . . . . . . . 8 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ 𝑦 = 𝐷))
8133a1d 25 . . . . . . . . . . . . 13 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ ((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∨ Β¬ ((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))))))
8243, 81cnfn2dd 36949 . . . . . . . . . . . 12 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ (π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡)))
83 tsbi4 36992 . . . . . . . . . . . . 13 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ ((Β¬ π‘₯ ∈ 𝐴 ∨ π‘₯ ∈ 𝐡) ∨ Β¬ (π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡)))
8483a1d 25 . . . . . . . . . . . 12 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ ((Β¬ π‘₯ ∈ 𝐴 ∨ π‘₯ ∈ 𝐡) ∨ Β¬ (π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡))))
8582, 84cnfn2dd 36949 . . . . . . . . . . 11 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ (Β¬ π‘₯ ∈ 𝐴 ∨ π‘₯ ∈ 𝐡)))
8642, 85cnfn1dd 36948 . . . . . . . . . 10 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ π‘₯ ∈ 𝐡))
87 tsan1 36997 . . . . . . . . . . . 12 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ ((Β¬ π‘₯ ∈ 𝐡 ∨ Β¬ 𝑦 = 𝐸) ∨ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)))
8887a1d 25 . . . . . . . . . . 11 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ ((Β¬ π‘₯ ∈ 𝐡 ∨ Β¬ 𝑦 = 𝐸) ∨ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))))
8975, 88cnf2dd 36947 . . . . . . . . . 10 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ (Β¬ π‘₯ ∈ 𝐡 ∨ Β¬ 𝑦 = 𝐸)))
9086, 89cnfn1dd 36948 . . . . . . . . 9 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ Β¬ 𝑦 = 𝐸))
91 tsbi4 36992 . . . . . . . . . . 11 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ ((Β¬ 𝑦 = 𝐷 ∨ 𝑦 = 𝐸) ∨ Β¬ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)))
9291a1d 25 . . . . . . . . . 10 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ ((Β¬ 𝑦 = 𝐷 ∨ 𝑦 = 𝐸) ∨ Β¬ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))))
9392or32dd 36950 . . . . . . . . 9 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ ((Β¬ 𝑦 = 𝐷 ∨ Β¬ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)) ∨ 𝑦 = 𝐸)))
9490, 93cnf2dd 36947 . . . . . . . 8 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ (Β¬ 𝑦 = 𝐷 ∨ Β¬ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))))
9580, 94cnfn1dd 36948 . . . . . . 7 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ (Β¬ βŠ₯ β†’ Β¬ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸)))
9647, 95contrd 36953 . . . . . 6 (Β¬ (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸))) β†’ βŠ₯)
9796efald2 36934 . . . . 5 (((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)))
98972alimi 1814 . . . 4 (βˆ€π‘₯βˆ€π‘¦((π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡) ∧ (π‘₯ ∈ 𝐴 β†’ (𝑦 = 𝐷 ↔ 𝑦 = 𝐸))) β†’ βˆ€π‘₯βˆ€π‘¦((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)))
9919, 98syl 17 . . 3 ((𝐴 = 𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 𝐷 = 𝐸) β†’ βˆ€π‘₯βˆ€π‘¦((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)))
100 eqopab2bw 5547 . . 3 ({⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷)} = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)} ↔ βˆ€π‘₯βˆ€π‘¦((π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)))
10199, 100sylibr 233 . 2 ((𝐴 = 𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 𝐷 = 𝐸) β†’ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷)} = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)})
102 df-mpt 5231 . 2 (π‘₯ ∈ 𝐴 ↦ 𝐷) = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷)}
103 df-mpt 5231 . 2 (π‘₯ ∈ 𝐡 ↦ 𝐸) = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸)}
104101, 102, 1033eqtr4g 2797 1 ((𝐴 = 𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 𝐷 = 𝐸) β†’ (π‘₯ ∈ 𝐴 ↦ 𝐷) = (π‘₯ ∈ 𝐡 ↦ 𝐸))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845  βˆ€wal 1539   = wceq 1541  βŠ₯wfal 1553   ∈ wcel 2106  β„²wnfc 2883  βˆ€wral 3061  {copab 5209   ↦ cmpt 5230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-opab 5210  df-mpt 5231
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator