Metamath Proof Explorer

Theorem mptbi12f

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

Ref Expression
Hypotheses mptbi12f.1 ⊒ β„² π‘₯ 𝐴
mptbi12f.2 ⊒ β„² π‘₯ 𝐡
Assertion mptbi12f ( ( 𝐴 = 𝐡 ∧ βˆ€ π‘₯ ∈ 𝐴 𝐷 = 𝐸 ) β†’ ( π‘₯ ∈ 𝐴 ↦ 𝐷 ) = ( π‘₯ ∈ 𝐡 ↦ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 mptbi12f.1 ⊒ β„² π‘₯ 𝐴
2 mptbi12f.2 ⊒ β„² π‘₯ 𝐡
3 1 2 nfeq ⊒ β„² π‘₯ 𝐴 = 𝐡
4 eleq2 ⊒ ( 𝐴 = 𝐡 β†’ ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) )
5 3 4 alrimi ⊒ ( 𝐴 = 𝐡 β†’ βˆ€ π‘₯ ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) )
6 ax-5 ⊒ ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) β†’ βˆ€ 𝑦 ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) )
7 5 6 sylg ⊒ ( 𝐴 = 𝐡 β†’ βˆ€ π‘₯ βˆ€ 𝑦 ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) )
8 eqeq2 ⊒ ( 𝐷 = 𝐸 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) )
9 8 alrimiv ⊒ ( 𝐷 = 𝐸 β†’ βˆ€ 𝑦 ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) )
10 9 ralimi ⊒ ( βˆ€ π‘₯ ∈ 𝐴 𝐷 = 𝐸 β†’ βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) )
11 df-ral ⊒ ( βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ↔ βˆ€ π‘₯ ( π‘₯ ∈ 𝐴 β†’ βˆ€ 𝑦 ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) )
12 10 11 sylib ⊒ ( βˆ€ π‘₯ ∈ 𝐴 𝐷 = 𝐸 β†’ βˆ€ π‘₯ ( π‘₯ ∈ 𝐴 β†’ βˆ€ 𝑦 ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) )
13 19.21v ⊒ ( βˆ€ 𝑦 ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ↔ ( π‘₯ ∈ 𝐴 β†’ βˆ€ 𝑦 ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) )
14 13 albii ⊒ ( βˆ€ π‘₯ βˆ€ 𝑦 ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ↔ βˆ€ π‘₯ ( π‘₯ ∈ 𝐴 β†’ βˆ€ 𝑦 ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) )
15 12 14 sylibr ⊒ ( βˆ€ π‘₯ ∈ 𝐴 𝐷 = 𝐸 β†’ βˆ€ π‘₯ βˆ€ 𝑦 ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) )
16 id ⊒ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) )
17 16 alanimi ⊒ ( ( βˆ€ 𝑦 ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ βˆ€ 𝑦 ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ βˆ€ 𝑦 ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) )
18 17 alanimi ⊒ ( ( βˆ€ π‘₯ βˆ€ 𝑦 ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ βˆ€ π‘₯ βˆ€ 𝑦 ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ βˆ€ π‘₯ βˆ€ 𝑦 ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) )
19 7 15 18 syl2an ⊒ ( ( 𝐴 = 𝐡 ∧ βˆ€ π‘₯ ∈ 𝐴 𝐷 = 𝐸 ) β†’ βˆ€ π‘₯ βˆ€ 𝑦 ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) )
20 tsan2 ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( π‘₯ ∈ 𝐴 ∨ Β¬ ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ) )
21 20 ord ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ π‘₯ ∈ 𝐴 β†’ Β¬ ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ) )
22 tsbi2 ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ∨ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ∨ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) )
23 22 ord ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ∨ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) )
24 23 a1dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ∨ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) β†’ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) ) )
25 ax-1 ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ∨ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) β†’ Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) ) )
26 24 25 contrd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ∨ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) )
27 26 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ π‘₯ ∈ 𝐴 β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ∨ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) )
28 21 27 cnf1dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ π‘₯ ∈ 𝐴 β†’ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) )
29 simplim ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) )
30 29 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ ( π‘₯ ∈ 𝐴 ∨ Β¬ π‘₯ ∈ 𝐡 ) β†’ ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) ) )
31 tsbi3 ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∨ Β¬ π‘₯ ∈ 𝐡 ) ∨ Β¬ ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ) )
32 31 ord ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ ( π‘₯ ∈ 𝐴 ∨ Β¬ π‘₯ ∈ 𝐡 ) β†’ Β¬ ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ) )
33 tsan2 ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∨ Β¬ ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) ) )
34 33 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ ( π‘₯ ∈ 𝐴 ∨ Β¬ π‘₯ ∈ 𝐡 ) β†’ ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∨ Β¬ ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) ) ) )
35 32 34 cnf1dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ ( π‘₯ ∈ 𝐴 ∨ Β¬ π‘₯ ∈ 𝐡 ) β†’ Β¬ ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) ) )
36 30 35 contrd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( π‘₯ ∈ 𝐴 ∨ Β¬ π‘₯ ∈ 𝐡 ) )
37 36 ord ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ π‘₯ ∈ 𝐴 β†’ Β¬ π‘₯ ∈ 𝐡 ) )
38 tsan2 ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( π‘₯ ∈ 𝐡 ∨ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) )
39 38 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ π‘₯ ∈ 𝐴 β†’ ( π‘₯ ∈ 𝐡 ∨ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) )
40 37 39 cnf1dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ π‘₯ ∈ 𝐴 β†’ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) )
41 28 40 contrd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ π‘₯ ∈ 𝐴 )
42 41 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ π‘₯ ∈ 𝐴 ) )
43 29 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) ) )
44 tsan3 ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ∨ Β¬ ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) ) )
45 44 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ ( ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ∨ Β¬ ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) ) ) )
46 43 45 cnfn2dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) )
47 42 46 mpdd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) )
48 notnotr ⊒ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) )
49 48 a1i ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) )
50 38 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ ( π‘₯ ∈ 𝐡 ∨ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) )
51 49 50 cnfn2dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ π‘₯ ∈ 𝐡 ) )
52 36 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ ( π‘₯ ∈ 𝐴 ∨ Β¬ π‘₯ ∈ 𝐡 ) ) )
53 51 52 cnfn2dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ π‘₯ ∈ 𝐴 ) )
54 tsan3 ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( 𝑦 = 𝐸 ∨ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) )
55 54 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ ( 𝑦 = 𝐸 ∨ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) )
56 49 55 cnfn2dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ 𝑦 = 𝐸 ) )
57 29 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) ) )
58 44 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ ( ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ∨ Β¬ ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) ) ) )
59 57 58 cnfn2dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) )
60 53 59 mpdd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) )
61 tsbi3 ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( ( 𝑦 = 𝐷 ∨ Β¬ 𝑦 = 𝐸 ) ∨ Β¬ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) )
62 61 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ ( ( 𝑦 = 𝐷 ∨ Β¬ 𝑦 = 𝐸 ) ∨ Β¬ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) )
63 60 62 cnfn2dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ ( 𝑦 = 𝐷 ∨ Β¬ 𝑦 = 𝐸 ) ) )
64 56 63 cnfn2dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ 𝑦 = 𝐷 ) )
65 53 64 jcad ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ) )
66 ax-1 ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) ) )
67 tsim3 ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ∨ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) ) )
68 67 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ ( Β¬ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ∨ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) ) ) )
69 66 68 cnf2dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ Β¬ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) )
70 tsbi1 ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( ( Β¬ ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ∨ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ∨ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) )
71 70 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ ( ( Β¬ ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ∨ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ∨ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) ) )
72 69 71 cnf2dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ ( Β¬ ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ∨ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) )
73 49 72 cnfn2dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) β†’ Β¬ ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ) )
74 65 73 contrd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) )
75 74 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ Β¬ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) )
76 26 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ∨ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) )
77 75 76 cnf2dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ) )
78 tsan3 ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( 𝑦 = 𝐷 ∨ Β¬ ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ) )
79 78 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ ( 𝑦 = 𝐷 ∨ Β¬ ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ) ) )
80 77 79 cnfn2dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ 𝑦 = 𝐷 ) )
81 33 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∨ Β¬ ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) ) ) )
82 43 81 cnfn2dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ) )
83 tsbi4 ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( ( Β¬ π‘₯ ∈ 𝐴 ∨ π‘₯ ∈ 𝐡 ) ∨ Β¬ ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ) )
84 83 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ ( ( Β¬ π‘₯ ∈ 𝐴 ∨ π‘₯ ∈ 𝐡 ) ∨ Β¬ ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ) ) )
85 82 84 cnfn2dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ ( Β¬ π‘₯ ∈ 𝐴 ∨ π‘₯ ∈ 𝐡 ) ) )
86 42 85 cnfn1dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ π‘₯ ∈ 𝐡 ) )
87 tsan1 ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( ( Β¬ π‘₯ ∈ 𝐡 ∨ Β¬ 𝑦 = 𝐸 ) ∨ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) )
88 87 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ ( ( Β¬ π‘₯ ∈ 𝐡 ∨ Β¬ 𝑦 = 𝐸 ) ∨ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) )
89 75 88 cnf2dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ ( Β¬ π‘₯ ∈ 𝐡 ∨ Β¬ 𝑦 = 𝐸 ) ) )
90 86 89 cnfn1dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ Β¬ 𝑦 = 𝐸 ) )
91 tsbi4 ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( ( Β¬ 𝑦 = 𝐷 ∨ 𝑦 = 𝐸 ) ∨ Β¬ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) )
92 91 a1d ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ ( ( Β¬ 𝑦 = 𝐷 ∨ 𝑦 = 𝐸 ) ∨ Β¬ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) )
93 92 or32dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ ( ( Β¬ 𝑦 = 𝐷 ∨ Β¬ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ∨ 𝑦 = 𝐸 ) ) )
94 90 93 cnf2dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ ( Β¬ 𝑦 = 𝐷 ∨ Β¬ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) )
95 80 94 cnfn1dd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ ( Β¬ βŠ₯ β†’ Β¬ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) )
96 47 95 contrd ⊒ ( Β¬ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) ) β†’ βŠ₯ )
97 96 efald2 ⊒ ( ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) )
98 97 2alimi ⊒ ( βˆ€ π‘₯ βˆ€ 𝑦 ( ( π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 β†’ ( 𝑦 = 𝐷 ↔ 𝑦 = 𝐸 ) ) ) β†’ βˆ€ π‘₯ βˆ€ 𝑦 ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) )
99 19 98 syl ⊒ ( ( 𝐴 = 𝐡 ∧ βˆ€ π‘₯ ∈ 𝐴 𝐷 = 𝐸 ) β†’ βˆ€ π‘₯ βˆ€ 𝑦 ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) )
100 eqopab2bw ⊒ ( { ⟨ π‘₯ , 𝑦 ⟩ ∣ ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) } = { ⟨ π‘₯ , 𝑦 ⟩ ∣ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) } ↔ βˆ€ π‘₯ βˆ€ 𝑦 ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) ) )
101 99 100 sylibr ⊒ ( ( 𝐴 = 𝐡 ∧ βˆ€ π‘₯ ∈ 𝐴 𝐷 = 𝐸 ) β†’ { ⟨ π‘₯ , 𝑦 ⟩ ∣ ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) } = { ⟨ π‘₯ , 𝑦 ⟩ ∣ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) } )
102 df-mpt ⊒ ( π‘₯ ∈ 𝐴 ↦ 𝐷 ) = { ⟨ π‘₯ , 𝑦 ⟩ ∣ ( π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐷 ) }
103 df-mpt ⊒ ( π‘₯ ∈ 𝐡 ↦ 𝐸 ) = { ⟨ π‘₯ , 𝑦 ⟩ ∣ ( π‘₯ ∈ 𝐡 ∧ 𝑦 = 𝐸 ) }
104 101 102 103 3eqtr4g ⊒ ( ( 𝐴 = 𝐡 ∧ βˆ€ π‘₯ ∈ 𝐴 𝐷 = 𝐸 ) β†’ ( π‘₯ ∈ 𝐴 ↦ 𝐷 ) = ( π‘₯ ∈ 𝐡 ↦ 𝐸 ) )