Metamath Proof Explorer

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 
|- ( w = <. x , y , z >. -> D = E )
Assertion mpt3mpt 
|- ( w e. ( ( A X. B ) X. C ) |-> D ) = ( x e. A , y e. B , z e. C |-> E )

Proof

Step Hyp Ref Expression
1 mpt3mpt.1 
 |-  ( w = <. x , y , z >. -> D = E )
2 el2xptp 
 |-  ( w e. ( ( A X. B ) X. C ) <-> E. x e. A E. y e. B E. z e. C w = <. x , y , z >. )
3 2 anbi1i 
 |-  ( ( w e. ( ( A X. B ) X. C ) /\ t = D ) <-> ( E. x e. A E. y e. B E. z e. C w = <. x , y , z >. /\ t = D ) )
4 r19.41v 
 |-  ( E. x e. A ( E. y e. B E. z e. C w = <. x , y , z >. /\ t = D ) <-> ( E. x e. A E. y e. B E. z e. C w = <. x , y , z >. /\ t = D ) )
5 r19.41v 
 |-  ( E. y e. B ( E. z e. C w = <. x , y , z >. /\ t = D ) <-> ( E. y e. B E. z e. C w = <. x , y , z >. /\ t = D ) )
6 r19.41v 
 |-  ( E. z e. C ( w = <. x , y , z >. /\ t = D ) <-> ( E. z e. C w = <. x , y , z >. /\ t = D ) )
7 1 eqeq2d 
 |-  ( w = <. x , y , z >. -> ( t = D <-> t = E ) )
8 7 pm5.32i 
 |-  ( ( w = <. x , y , z >. /\ t = D ) <-> ( w = <. x , y , z >. /\ t = E ) )
9 8 rexbii 
 |-  ( E. z e. C ( w = <. x , y , z >. /\ t = D ) <-> E. z e. C ( w = <. x , y , z >. /\ t = E ) )
10 6 9 bitr3i 
 |-  ( ( E. z e. C w = <. x , y , z >. /\ t = D ) <-> E. z e. C ( w = <. x , y , z >. /\ t = E ) )
11 10 rexbii 
 |-  ( E. y e. B ( E. z e. C w = <. x , y , z >. /\ t = D ) <-> E. y e. B E. z e. C ( w = <. x , y , z >. /\ t = E ) )
12 5 11 bitr3i 
 |-  ( ( E. y e. B E. z e. C w = <. x , y , z >. /\ t = D ) <-> E. y e. B E. z e. C ( w = <. x , y , z >. /\ t = E ) )
13 12 rexbii 
 |-  ( E. x e. A ( E. y e. B E. z e. C w = <. x , y , z >. /\ t = D ) <-> E. x e. A E. y e. B E. z e. C ( w = <. x , y , z >. /\ t = E ) )
14 3 4 13 3bitr2i 
 |-  ( ( w e. ( ( A X. B ) X. C ) /\ t = D ) <-> E. x e. A E. y e. B E. z e. C ( w = <. x , y , z >. /\ t = E ) )
15 14 opabbii 
 |-  { <. w , t >. | ( w e. ( ( A X. B ) X. C ) /\ t = D ) } = { <. w , t >. | E. x e. A E. y e. B E. z e. C ( w = <. x , y , z >. /\ t = E ) }
16 df-mpt 
 |-  ( w e. ( ( A X. B ) X. C ) |-> D ) = { <. w , t >. | ( w e. ( ( A X. B ) X. C ) /\ t = D ) }
17 df-mpt3 
 |-  ( x e. A , y e. B , z e. C |-> E ) = { <. w , t >. | E. x e. A E. y e. B E. z e. C ( w = <. x , y , z >. /\ t = E ) }
18 15 16 17 3eqtr4i 
 |-  ( w e. ( ( A X. B ) X. C ) |-> D ) = ( x e. A , y e. B , z e. C |-> E )