Definition df-bj-mpt3 33074

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

Assertion

Ref	Expression
df-bj-mpt3	|- ( x e. A , y e. B , z e. C |-> D ) = { <. s , t >. | E. x e. A E. y e. B E. z e. C ( s = <. x , y , z >. /\ t = D ) }

Distinct variable groups:   t, s, x   y, s, t   z, s, t   A, s, t   B, s, t   C, s, t   D, s, t

Allowed substitution hints:   A( x, y, z)   B( x, y, z)   C( x, y, z)   D( x, y, z)

Detailed syntax breakdown of Definition df-bj-mpt3

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar x
2		vy	. . 3 setvar y
3		vz	. . 3 setvar z
4		cA	. . 3 class A
5		cB	. . 3 class B
6		cC	. . 3 class C
7		cD	. . 3 class D
8	1, 2, 3, 4, 5, 6, 7	cmpt3 33073	. 2 class ( x e. A , y e. B , z e. C |-> D )
9		vs	. . . . . . . . 9 setvar s
10	9	cv 1482	. . . . . . . 8 class s
11	1	cv 1482	. . . . . . . . 9 class x
12	2	cv 1482	. . . . . . . . 9 class y
13	3	cv 1482	. . . . . . . . 9 class z
14	11, 12, 13	cotp 4185	. . . . . . . 8 class <. x , y , z >.
15	10, 14	wceq 1483	. . . . . . 7 wff s = <. x , y , z >.
16		vt	. . . . . . . . 9 setvar t
17	16	cv 1482	. . . . . . . 8 class t
18	17, 7	wceq 1483	. . . . . . 7 wff t = D
19	15, 18	wa 384	. . . . . 6 wff ( s = <. x , y , z >. /\ t = D )
20	19, 3, 6	wrex 2913	. . . . 5 wff E. z e. C ( s = <. x , y , z >. /\ t = D )
21	20, 2, 5	wrex 2913	. . . 4 wff E. y e. B E. z e. C ( s = <. x , y , z >. /\ t = D )
22	21, 1, 4	wrex 2913	. . 3 wff E. x e. A E. y e. B E. z e. C ( s = <. x , y , z >. /\ t = D )
23	22, 9, 16	copab 4712	. 2 class { <. s , t >. | E. x e. A E. y e. B E. z e. C ( s = <. x , y , z >. /\ t = D ) }
24	8, 23	wceq 1483	1 wff ( x e. A , y e. B , z e. C |-> D ) = { <. s , t >. | E. x e. A E. y e. B E. z e. C ( s = <. x , y , z >. /\ t = D ) }

This definition is referenced by: (None)