Metamath Proof Explorer

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 
|- ( 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 ) }

Detailed syntax breakdown

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