Theorem mpt3mpt

Description: Express a three-argument function as a one-argument function, or vice-versa. (Contributed by BTernaryTau, 7-Sep-2026)

	Ref	Expression
Hypothesis	mpt3mpt.1	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → 𝐷 = 𝐸 )
Assertion	mpt3mpt	⊢ ( 𝑤 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↦ 𝐷 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		mpt3mpt.1	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → 𝐷 = 𝐸 )
2		el2xptp	⊢ ( 𝑤 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )
3	2	anbi1i	⊢ ( ( 𝑤 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑡 = 𝐷 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 ) )
4		r19.41v	⊢ ( ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 ) )
5		r19.41v	⊢ ( ∃ 𝑦 ∈ 𝐵 ( ∃ 𝑧 ∈ 𝐶 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 ) ↔ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 ) )
6		r19.41v	⊢ ( ∃ 𝑧 ∈ 𝐶 ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 ) ↔ ( ∃ 𝑧 ∈ 𝐶 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 ) )
7	1	eqeq2d	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 𝑡 = 𝐷 ↔ 𝑡 = 𝐸 ) )
8	7	pm5.32i	⊢ ( ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐸 ) )
9	8	rexbii	⊢ ( ∃ 𝑧 ∈ 𝐶 ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 ) ↔ ∃ 𝑧 ∈ 𝐶 ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐸 ) )
10	6 9	bitr3i	⊢ ( ( ∃ 𝑧 ∈ 𝐶 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 ) ↔ ∃ 𝑧 ∈ 𝐶 ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐸 ) )
11	10	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐵 ( ∃ 𝑧 ∈ 𝐶 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐸 ) )
12	5 11	bitr3i	⊢ ( ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐸 ) )
13	12	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐸 ) )
14	3 4 13	3bitr2i	⊢ ( ( 𝑤 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑡 = 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐸 ) )
15	14	opabbii	⊢ { ⟨ 𝑤 , 𝑡 ⟩ ∣ ( 𝑤 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑡 = 𝐷 ) } = { ⟨ 𝑤 , 𝑡 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐸 ) }
16		df-mpt	⊢ ( 𝑤 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↦ 𝐷 ) = { ⟨ 𝑤 , 𝑡 ⟩ ∣ ( 𝑤 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑡 = 𝐷 ) }
17		df-mpt3	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐸 ) = { ⟨ 𝑤 , 𝑡 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐸 ) }
18	15 16 17	3eqtr4i	⊢ ( 𝑤 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↦ 𝐷 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐸 )