Definition df-bj-mpt3

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

	Ref	Expression
Assertion	df-bj-mpt3	$$⊢\left(x\in A,y\in B,z\in C⟼D\right)=\left\{⟨s,t⟩|\exists x\in A\exists y\in B\exists z\in C\left(s=⟨x,y,z⟩\wedge t=D\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		vy	$$setvary$$
3		cB	$$classB$$
4		vz	$$setvarz$$
5		cC	$$classC$$
6		cD	$$classD$$
7	0 2 4 1 3 5 6	cmpt3	$$class\left(x\in A,y\in B,z\in C⟼D\right)$$
8		vs	$$setvars$$
9		vt	$$setvart$$
10	8	cv	$$setvars$$
11	0	cv	$$setvarx$$
12	2	cv	$$setvary$$
13	4	cv	$$setvarz$$
14	11 12 13	cotp	$$class⟨x,y,z⟩$$
15	10 14	wceq	$$wffs=⟨x,y,z⟩$$
16	9	cv	$$setvart$$
17	16 6	wceq	$$wfft=D$$
18	15 17	wa	$$wff\left(s=⟨x,y,z⟩\wedge t=D\right)$$
19	18 4 5	wrex	$$wff\exists z\in C\left(s=⟨x,y,z⟩\wedge t=D\right)$$
20	19 2 3	wrex	$$wff\exists y\in B\exists z\in C\left(s=⟨x,y,z⟩\wedge t=D\right)$$
21	20 0 1	wrex	$$wff\exists x\in A\exists y\in B\exists z\in C\left(s=⟨x,y,z⟩\wedge t=D\right)$$
22	21 8 9	copab	$$class\left\{⟨s,t⟩|\exists x\in A\exists y\in B\exists z\in C\left(s=⟨x,y,z⟩\wedge t=D\right)\right\}$$
23	7 22	wceq	$$wff\left(x\in A,y\in B,z\in C⟼D\right)=\left\{⟨s,t⟩|\exists x\in A\exists y\in B\exists z\in C\left(s=⟨x,y,z⟩\wedge t=D\right)\right\}$$