Theorem mpomptx2

Description: Express a two-argument function as a one-argument function, or vice-versa. In this version A ( y ) is not assumed to be constant w.r.t y , analogous to mpomptx . (Contributed by AV, 30-Mar-2019)

	Ref	Expression
Hypothesis	mpomptx2.1	|- ( z = <. x , y >. -> C = D )
Assertion	mpomptx2	|- ( z e. U_ y e. B ( A X. { y } ) |-> C ) = ( x e. A , y e. B |-> D )

Proof

Step	Hyp	Ref	Expression
1		mpomptx2.1	|- ( z = <. x , y >. -> C = D )
2		df-mpt	|- ( z e. U_ y e. B ( A X. { y } ) |-> C ) = { <. z , w >. | ( z e. U_ y e. B ( A X. { y } ) /\ w = C ) }
3		df-mpo	|- ( x e. A , y e. B |-> D ) = { <. <. x , y >. , w >. | ( ( x e. A /\ y e. B ) /\ w = D ) }
4		eliunxp2	|- ( z e. U_ y e. B ( A X. { y } ) <-> E. x E. y ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
5	4	anbi1i	|- ( ( z e. U_ y e. B ( A X. { y } ) /\ w = C ) <-> ( E. x E. y ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) )
6		19.41vv	|- ( E. x E. y ( ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) <-> ( E. x E. y ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) )
7		anass	|- ( ( ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) <-> ( z = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) )
8	1	eqeq2d	|- ( z = <. x , y >. -> ( w = C <-> w = D ) )
9	8	anbi2d	|- ( z = <. x , y >. -> ( ( ( x e. A /\ y e. B ) /\ w = C ) <-> ( ( x e. A /\ y e. B ) /\ w = D ) ) )
10	9	pm5.32i	|- ( ( z = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) <-> ( z = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ w = D ) ) )
11	7 10	bitri	|- ( ( ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) <-> ( z = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ w = D ) ) )
12	11	2exbii	|- ( E. x E. y ( ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) <-> E. x E. y ( z = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ w = D ) ) )
13	5 6 12	3bitr2i	|- ( ( z e. U_ y e. B ( A X. { y } ) /\ w = C ) <-> E. x E. y ( z = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ w = D ) ) )
14	13	opabbii	|- { <. z , w >. | ( z e. U_ y e. B ( A X. { y } ) /\ w = C ) } = { <. z , w >. | E. x E. y ( z = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ w = D ) ) }
15		dfoprab2	|- { <. <. x , y >. , w >. | ( ( x e. A /\ y e. B ) /\ w = D ) } = { <. z , w >. | E. x E. y ( z = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ w = D ) ) }
16	14 15	eqtr4i	|- { <. z , w >. | ( z e. U_ y e. B ( A X. { y } ) /\ w = C ) } = { <. <. x , y >. , w >. | ( ( x e. A /\ y e. B ) /\ w = D ) }
17	3 16	eqtr4i	|- ( x e. A , y e. B |-> D ) = { <. z , w >. | ( z e. U_ y e. B ( A X. { y } ) /\ w = C ) }
18	2 17	eqtr4i	|- ( z e. U_ y e. B ( A X. { y } ) |-> C ) = ( x e. A , y e. B |-> D )