# Metamath Proof Explorer

## Theorem mpomptx

Description: Express a two-argument function as a one-argument function, or vice-versa. In this version B ( x ) is not assumed to be constant w.r.t x . (Contributed by Mario Carneiro, 29-Dec-2014)

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

### Proof

Step Hyp Ref Expression
1 mpompt.1
` |-  ( z = <. x , y >. -> C = D )`
2 df-mpt
` |-  ( z e. U_ x e. A ( { x } X. B ) |-> C ) = { <. z , w >. | ( z e. U_ x e. A ( { x } X. B ) /\ w = C ) }`
3 df-mpo
` |-  ( x e. A , y e. B |-> D ) = { <. <. x , y >. , w >. | ( ( x e. A /\ y e. B ) /\ w = D ) }`
4 eliunxp
` |-  ( z e. U_ x e. A ( { x } X. B ) <-> E. x E. y ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) )`
5 4 anbi1i
` |-  ( ( z e. U_ x e. A ( { x } X. B ) /\ 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_ x e. A ( { x } X. B ) /\ 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_ x e. A ( { x } X. B ) /\ 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_ x e. A ( { x } X. B ) /\ 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_ x e. A ( { x } X. B ) /\ w = C ) }`
18 2 17 eqtr4i
` |-  ( z e. U_ x e. A ( { x } X. B ) |-> C ) = ( x e. A , y e. B |-> D )`