Definition df-bj-mpt3 37123

Description: Define maps-to notation for functions with three arguments. See df-mpt 5225 and df-mpo 7437 for functions with one and two arguments respectively. This definition is analogous to bj-dfmpoa 37120. (Contributed by BJ, 11-Apr-2020.)

Assertion

Ref	Expression
df-bj-mpt3	⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷) = {⟨𝑠, 𝑡⟩ ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝑠 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑡 = 𝐷)}

Distinct variable groups:   𝑡,𝑠,𝑥   𝑦,𝑠,𝑡   𝑧,𝑠,𝑡   𝐴,𝑠,𝑡   𝐵,𝑠,𝑡   𝐶,𝑠,𝑡   𝐷,𝑠,𝑡

Allowed substitution hints:   𝐴(𝑥,𝑦,𝑧)   𝐵(𝑥,𝑦,𝑧)   𝐶(𝑥,𝑦,𝑧)   𝐷(𝑥,𝑦,𝑧)

Detailed syntax breakdown of Definition df-bj-mpt3

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar 𝑥
2		vy	. . 3 setvar 𝑦
3		vz	. . 3 setvar 𝑧
4		cA	. . 3 class 𝐴
5		cB	. . 3 class 𝐵
6		cC	. . 3 class 𝐶
7		cD	. . 3 class 𝐷
8	1, 2, 3, 4, 5, 6, 7	cmpt3 37122	. 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷)
9		vs	. . . . . . . . 9 setvar 𝑠
10	9	cv 1538	. . . . . . . 8 class 𝑠
11	1	cv 1538	. . . . . . . . 9 class 𝑥
12	2	cv 1538	. . . . . . . . 9 class 𝑦
13	3	cv 1538	. . . . . . . . 9 class 𝑧
14	11, 12, 13	cotp 4633	. . . . . . . 8 class ⟨𝑥, 𝑦, 𝑧⟩
15	10, 14	wceq 1539	. . . . . . 7 wff 𝑠 = ⟨𝑥, 𝑦, 𝑧⟩
16		vt	. . . . . . . . 9 setvar 𝑡
17	16	cv 1538	. . . . . . . 8 class 𝑡
18	17, 7	wceq 1539	. . . . . . 7 wff 𝑡 = 𝐷
19	15, 18	wa 395	. . . . . 6 wff (𝑠 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑡 = 𝐷)
20	19, 3, 6	wrex 3069	. . . . 5 wff ∃𝑧 ∈ 𝐶 (𝑠 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑡 = 𝐷)
21	20, 2, 5	wrex 3069	. . . 4 wff ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝑠 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑡 = 𝐷)
22	21, 1, 4	wrex 3069	. . 3 wff ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝑠 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑡 = 𝐷)
23	22, 9, 16	copab 5204	. 2 class {⟨𝑠, 𝑡⟩ ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝑠 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑡 = 𝐷)}
24	8, 23	wceq 1539	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷) = {⟨𝑠, 𝑡⟩ ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝑠 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑡 = 𝐷)}

This definition is referenced by: (None)