Metamath Proof Explorer

Theorem mpt3eqdv

Description: An equality deduction for maps-to notation. (Contributed by BTernaryTau, 8-Sep-2026)

Ref Expression
Hypotheses mpt3eqdv.1 ⊢ ( 𝜑 → 𝐴 = 𝐸 )
mpt3eqdv.2 ⊢ ( 𝜑 → 𝐵 = 𝐹 )
mpt3eqdv.3 ⊢ ( 𝜑 → 𝐶 = 𝐺 )
mpt3eqdv.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) → 𝐷 = 𝐻 )
Assertion mpt3eqdv ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 ) = ( 𝑥 ∈ 𝐸 , 𝑦 ∈ 𝐹 , 𝑧 ∈ 𝐺 ↦ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 mpt3eqdv.1 ⊢ ( 𝜑 → 𝐴 = 𝐸 )
2 mpt3eqdv.2 ⊢ ( 𝜑 → 𝐵 = 𝐹 )
3 mpt3eqdv.3 ⊢ ( 𝜑 → 𝐶 = 𝐺 )
4 mpt3eqdv.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) → 𝐷 = 𝐻 )
5 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = 𝐹 )
6 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 = 𝐺 )
7 3an4anass ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) )
8 13an22anass ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) )
9 7 8 bitr4i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) ↔ ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) )
10 4 eqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) → ( 𝑤 = 𝐷 ↔ 𝑤 = 𝐻 ) )
11 10 anbi2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) → ( ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐻 ) ) )
12 9 11 sylbi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) → ( ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐻 ) ) )
13 6 12 rexeqbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ∃ 𝑧 ∈ 𝐺 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐻 ) ) )
14 13 3expa ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ∃ 𝑧 ∈ 𝐺 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐻 ) ) )
15 5 14 rexeqbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ∃ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐺 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐻 ) ) )
16 1 15 rexeqbidva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐺 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐻 ) ) )
17 16 opabbidv ⊢ ( 𝜑 → { ⟨ 𝑣 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) } = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐺 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐻 ) } )
18 df-mpt3 ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 ) = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) }
19 df-mpt3 ⊢ ( 𝑥 ∈ 𝐸 , 𝑦 ∈ 𝐹 , 𝑧 ∈ 𝐺 ↦ 𝐻 ) = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐺 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐻 ) }
20 17 18 19 3eqtr4g ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 ) = ( 𝑥 ∈ 𝐸 , 𝑦 ∈ 𝐹 , 𝑧 ∈ 𝐺 ↦ 𝐻 ) )