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 35562
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 2992 . . . . . . 7 𝑥 𝐴 = 𝐵
4 eleq2 2902 . . . . . . 7 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
53, 4alrimi 2214 . . . . . 6 (𝐴 = 𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
6 ax-5 1911 . . . . . 6 ((𝑥𝐴𝑥𝐵) → ∀𝑦(𝑥𝐴𝑥𝐵))
75, 6sylg 1824 . . . . 5 (𝐴 = 𝐵 → ∀𝑥𝑦(𝑥𝐴𝑥𝐵))
8 eqeq2 2834 . . . . . . . . 9 (𝐷 = 𝐸 → (𝑦 = 𝐷𝑦 = 𝐸))
98alrimiv 1928 . . . . . . . 8 (𝐷 = 𝐸 → ∀𝑦(𝑦 = 𝐷𝑦 = 𝐸))
109ralimi 3152 . . . . . . 7 (∀𝑥𝐴 𝐷 = 𝐸 → ∀𝑥𝐴𝑦(𝑦 = 𝐷𝑦 = 𝐸))
11 df-ral 3135 . . . . . . 7 (∀𝑥𝐴𝑦(𝑦 = 𝐷𝑦 = 𝐸) ↔ ∀𝑥(𝑥𝐴 → ∀𝑦(𝑦 = 𝐷𝑦 = 𝐸)))
1210, 11sylib 221 . . . . . 6 (∀𝑥𝐴 𝐷 = 𝐸 → ∀𝑥(𝑥𝐴 → ∀𝑦(𝑦 = 𝐷𝑦 = 𝐸)))
13 19.21v 1940 . . . . . . 7 (∀𝑦(𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸)) ↔ (𝑥𝐴 → ∀𝑦(𝑦 = 𝐷𝑦 = 𝐸)))
1413albii 1821 . . . . . 6 (∀𝑥𝑦(𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸)) ↔ ∀𝑥(𝑥𝐴 → ∀𝑦(𝑦 = 𝐷𝑦 = 𝐸)))
1512, 14sylibr 237 . . . . 5 (∀𝑥𝐴 𝐷 = 𝐸 → ∀𝑥𝑦(𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸)))
16 id 22 . . . . . . 7 (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))))
1716alanimi 1818 . . . . . 6 ((∀𝑦(𝑥𝐴𝑥𝐵) ∧ ∀𝑦(𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ∀𝑦((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))))
1817alanimi 1818 . . . . 5 ((∀𝑥𝑦(𝑥𝐴𝑥𝐵) ∧ ∀𝑥𝑦(𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ∀𝑥𝑦((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))))
197, 15, 18syl2an 598 . . . 4 ((𝐴 = 𝐵 ∧ ∀𝑥𝐴 𝐷 = 𝐸) → ∀𝑥𝑦((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))))
20 tsan2 35538 . . . . . . . . . . . 12 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (𝑥𝐴 ∨ ¬ (𝑥𝐴𝑦 = 𝐷)))
2120ord 861 . . . . . . . . . . 11 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ 𝑥𝐴 → ¬ (𝑥𝐴𝑦 = 𝐷)))
22 tsbi2 35530 . . . . . . . . . . . . . . 15 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (((𝑥𝐴𝑦 = 𝐷) ∨ (𝑥𝐵𝑦 = 𝐸)) ∨ ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))))
2322ord 861 . . . . . . . . . . . . . 14 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ((𝑥𝐴𝑦 = 𝐷) ∨ (𝑥𝐵𝑦 = 𝐸)) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))))
2423a1dd 50 . . . . . . . . . . . . 13 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ((𝑥𝐴𝑦 = 𝐷) ∨ (𝑥𝐵𝑦 = 𝐸)) → (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸)))))
25 ax-1 6 . . . . . . . . . . . . 13 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ((𝑥𝐴𝑦 = 𝐷) ∨ (𝑥𝐵𝑦 = 𝐸)) → ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸)))))
2624, 25contrd 35493 . . . . . . . . . . . 12 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ∨ (𝑥𝐵𝑦 = 𝐸)))
2726a1d 25 . . . . . . . . . . 11 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ 𝑥𝐴 → ((𝑥𝐴𝑦 = 𝐷) ∨ (𝑥𝐵𝑦 = 𝐸))))
2821, 27cnf1dd 35486 . . . . . . . . . 10 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ 𝑥𝐴 → (𝑥𝐵𝑦 = 𝐸)))
29 simplim 170 . . . . . . . . . . . . . 14 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → ((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))))
3029a1d 25 . . . . . . . . . . . . 13 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ (𝑥𝐴 ∨ ¬ 𝑥𝐵) → ((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸)))))
31 tsbi3 35531 . . . . . . . . . . . . . . 15 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → ((𝑥𝐴 ∨ ¬ 𝑥𝐵) ∨ ¬ (𝑥𝐴𝑥𝐵)))
3231ord 861 . . . . . . . . . . . . . 14 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ (𝑥𝐴 ∨ ¬ 𝑥𝐵) → ¬ (𝑥𝐴𝑥𝐵)))
33 tsan2 35538 . . . . . . . . . . . . . . 15 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → ((𝑥𝐴𝑥𝐵) ∨ ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸)))))
3433a1d 25 . . . . . . . . . . . . . 14 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ (𝑥𝐴 ∨ ¬ 𝑥𝐵) → ((𝑥𝐴𝑥𝐵) ∨ ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))))))
3532, 34cnf1dd 35486 . . . . . . . . . . . . 13 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ (𝑥𝐴 ∨ ¬ 𝑥𝐵) → ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸)))))
3630, 35contrd 35493 . . . . . . . . . . . 12 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (𝑥𝐴 ∨ ¬ 𝑥𝐵))
3736ord 861 . . . . . . . . . . 11 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ 𝑥𝐴 → ¬ 𝑥𝐵))
38 tsan2 35538 . . . . . . . . . . . 12 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (𝑥𝐵 ∨ ¬ (𝑥𝐵𝑦 = 𝐸)))
3938a1d 25 . . . . . . . . . . 11 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ 𝑥𝐴 → (𝑥𝐵 ∨ ¬ (𝑥𝐵𝑦 = 𝐸))))
4037, 39cnf1dd 35486 . . . . . . . . . 10 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ 𝑥𝐴 → ¬ (𝑥𝐵𝑦 = 𝐸)))
4128, 40contrd 35493 . . . . . . . . 9 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → 𝑥𝐴)
4241a1d 25 . . . . . . . 8 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → 𝑥𝐴))
4329a1d 25 . . . . . . . . 9 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → ((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸)))))
44 tsan3 35539 . . . . . . . . . 10 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → ((𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸)) ∨ ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸)))))
4544a1d 25 . . . . . . . . 9 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → ((𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸)) ∨ ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))))))
4643, 45cnfn2dd 35489 . . . . . . . 8 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))))
4742, 46mpdd 43 . . . . . . 7 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → (𝑦 = 𝐷𝑦 = 𝐸)))
48 notnotr 132 . . . . . . . . . . . . . . . 16 (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → (𝑥𝐵𝑦 = 𝐸))
4948a1i 11 . . . . . . . . . . . . . . 15 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → (𝑥𝐵𝑦 = 𝐸)))
5038a1d 25 . . . . . . . . . . . . . . 15 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → (𝑥𝐵 ∨ ¬ (𝑥𝐵𝑦 = 𝐸))))
5149, 50cnfn2dd 35489 . . . . . . . . . . . . . 14 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → 𝑥𝐵))
5236a1d 25 . . . . . . . . . . . . . 14 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → (𝑥𝐴 ∨ ¬ 𝑥𝐵)))
5351, 52cnfn2dd 35489 . . . . . . . . . . . . 13 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → 𝑥𝐴))
54 tsan3 35539 . . . . . . . . . . . . . . . 16 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (𝑦 = 𝐸 ∨ ¬ (𝑥𝐵𝑦 = 𝐸)))
5554a1d 25 . . . . . . . . . . . . . . 15 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → (𝑦 = 𝐸 ∨ ¬ (𝑥𝐵𝑦 = 𝐸))))
5649, 55cnfn2dd 35489 . . . . . . . . . . . . . 14 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → 𝑦 = 𝐸))
5729a1d 25 . . . . . . . . . . . . . . . . 17 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → ((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸)))))
5844a1d 25 . . . . . . . . . . . . . . . . 17 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → ((𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸)) ∨ ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))))))
5957, 58cnfn2dd 35489 . . . . . . . . . . . . . . . 16 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))))
6053, 59mpdd 43 . . . . . . . . . . . . . . 15 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → (𝑦 = 𝐷𝑦 = 𝐸)))
61 tsbi3 35531 . . . . . . . . . . . . . . . 16 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → ((𝑦 = 𝐷 ∨ ¬ 𝑦 = 𝐸) ∨ ¬ (𝑦 = 𝐷𝑦 = 𝐸)))
6261a1d 25 . . . . . . . . . . . . . . 15 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → ((𝑦 = 𝐷 ∨ ¬ 𝑦 = 𝐸) ∨ ¬ (𝑦 = 𝐷𝑦 = 𝐸))))
6360, 62cnfn2dd 35489 . . . . . . . . . . . . . 14 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → (𝑦 = 𝐷 ∨ ¬ 𝑦 = 𝐸)))
6456, 63cnfn2dd 35489 . . . . . . . . . . . . 13 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → 𝑦 = 𝐷))
6553, 64jcad 516 . . . . . . . . . . . 12 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → (𝑥𝐴𝑦 = 𝐷)))
66 ax-1 6 . . . . . . . . . . . . . . 15 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸)))))
67 tsim3 35528 . . . . . . . . . . . . . . . 16 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸)) ∨ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸)))))
6867a1d 25 . . . . . . . . . . . . . . 15 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → (¬ ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸)) ∨ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))))))
6966, 68cnf2dd 35487 . . . . . . . . . . . . . 14 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → ¬ ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))))
70 tsbi1 35529 . . . . . . . . . . . . . . 15 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → ((¬ (𝑥𝐴𝑦 = 𝐷) ∨ ¬ (𝑥𝐵𝑦 = 𝐸)) ∨ ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))))
7170a1d 25 . . . . . . . . . . . . . 14 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → ((¬ (𝑥𝐴𝑦 = 𝐷) ∨ ¬ (𝑥𝐵𝑦 = 𝐸)) ∨ ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸)))))
7269, 71cnf2dd 35487 . . . . . . . . . . . . 13 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → (¬ (𝑥𝐴𝑦 = 𝐷) ∨ ¬ (𝑥𝐵𝑦 = 𝐸))))
7349, 72cnfn2dd 35489 . . . . . . . . . . . 12 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ¬ (𝑥𝐵𝑦 = 𝐸) → ¬ (𝑥𝐴𝑦 = 𝐷)))
7465, 73contrd 35493 . . . . . . . . . . 11 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → ¬ (𝑥𝐵𝑦 = 𝐸))
7574a1d 25 . . . . . . . . . 10 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → ¬ (𝑥𝐵𝑦 = 𝐸)))
7626a1d 25 . . . . . . . . . 10 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → ((𝑥𝐴𝑦 = 𝐷) ∨ (𝑥𝐵𝑦 = 𝐸))))
7775, 76cnf2dd 35487 . . . . . . . . 9 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → (𝑥𝐴𝑦 = 𝐷)))
78 tsan3 35539 . . . . . . . . . 10 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (𝑦 = 𝐷 ∨ ¬ (𝑥𝐴𝑦 = 𝐷)))
7978a1d 25 . . . . . . . . 9 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → (𝑦 = 𝐷 ∨ ¬ (𝑥𝐴𝑦 = 𝐷))))
8077, 79cnfn2dd 35489 . . . . . . . 8 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → 𝑦 = 𝐷))
8133a1d 25 . . . . . . . . . . . . 13 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → ((𝑥𝐴𝑥𝐵) ∨ ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))))))
8243, 81cnfn2dd 35489 . . . . . . . . . . . 12 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → (𝑥𝐴𝑥𝐵)))
83 tsbi4 35532 . . . . . . . . . . . . 13 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → ((¬ 𝑥𝐴𝑥𝐵) ∨ ¬ (𝑥𝐴𝑥𝐵)))
8483a1d 25 . . . . . . . . . . . 12 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → ((¬ 𝑥𝐴𝑥𝐵) ∨ ¬ (𝑥𝐴𝑥𝐵))))
8582, 84cnfn2dd 35489 . . . . . . . . . . 11 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → (¬ 𝑥𝐴𝑥𝐵)))
8642, 85cnfn1dd 35488 . . . . . . . . . 10 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → 𝑥𝐵))
87 tsan1 35537 . . . . . . . . . . . 12 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → ((¬ 𝑥𝐵 ∨ ¬ 𝑦 = 𝐸) ∨ (𝑥𝐵𝑦 = 𝐸)))
8887a1d 25 . . . . . . . . . . 11 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → ((¬ 𝑥𝐵 ∨ ¬ 𝑦 = 𝐸) ∨ (𝑥𝐵𝑦 = 𝐸))))
8975, 88cnf2dd 35487 . . . . . . . . . 10 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → (¬ 𝑥𝐵 ∨ ¬ 𝑦 = 𝐸)))
9086, 89cnfn1dd 35488 . . . . . . . . 9 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → ¬ 𝑦 = 𝐸))
91 tsbi4 35532 . . . . . . . . . . 11 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → ((¬ 𝑦 = 𝐷𝑦 = 𝐸) ∨ ¬ (𝑦 = 𝐷𝑦 = 𝐸)))
9291a1d 25 . . . . . . . . . 10 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → ((¬ 𝑦 = 𝐷𝑦 = 𝐸) ∨ ¬ (𝑦 = 𝐷𝑦 = 𝐸))))
9392or32dd 35490 . . . . . . . . 9 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → ((¬ 𝑦 = 𝐷 ∨ ¬ (𝑦 = 𝐷𝑦 = 𝐸)) ∨ 𝑦 = 𝐸)))
9490, 93cnf2dd 35487 . . . . . . . 8 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → (¬ 𝑦 = 𝐷 ∨ ¬ (𝑦 = 𝐷𝑦 = 𝐸))))
9580, 94cnfn1dd 35488 . . . . . . 7 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → (¬ ⊥ → ¬ (𝑦 = 𝐷𝑦 = 𝐸)))
9647, 95contrd 35493 . . . . . 6 (¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸))) → ⊥)
9796efald2 35474 . . . . 5 (((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸)))
98972alimi 1814 . . . 4 (∀𝑥𝑦((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴 → (𝑦 = 𝐷𝑦 = 𝐸))) → ∀𝑥𝑦((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸)))
9919, 98syl 17 . . 3 ((𝐴 = 𝐵 ∧ ∀𝑥𝐴 𝐷 = 𝐸) → ∀𝑥𝑦((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸)))
100 eqopab2bw 5412 . . 3 ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐷)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦 = 𝐸)} ↔ ∀𝑥𝑦((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐵𝑦 = 𝐸)))
10199, 100sylibr 237 . 2 ((𝐴 = 𝐵 ∧ ∀𝑥𝐴 𝐷 = 𝐸) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐷)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦 = 𝐸)})
102 df-mpt 5123 . 2 (𝑥𝐴𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐷)}
103 df-mpt 5123 . 2 (𝑥𝐵𝐸) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦 = 𝐸)}
104101, 102, 1033eqtr4g 2882 1 ((𝐴 = 𝐵 ∧ ∀𝑥𝐴 𝐷 = 𝐸) → (𝑥𝐴𝐷) = (𝑥𝐵𝐸))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  wal 1536   = wceq 1538  wfal 1550  wcel 2114  wnfc 2960  wral 3130  {copab 5104  cmpt 5122
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pr 5307
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-v 3471  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-op 4546  df-opab 5105  df-mpt 5123
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator