# Metamath Proof Explorer

## Theorem cbvmpox

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo allows B to be a function of x . (Contributed by NM, 29-Dec-2014)

Ref Expression
Hypotheses cbvmpox.1
`|- F/_ z B`
cbvmpox.2
`|- F/_ x D`
cbvmpox.3
`|- F/_ z C`
cbvmpox.4
`|- F/_ w C`
cbvmpox.5
`|- F/_ x E`
cbvmpox.6
`|- F/_ y E`
cbvmpox.7
`|- ( x = z -> B = D )`
cbvmpox.8
`|- ( ( x = z /\ y = w ) -> C = E )`
Assertion cbvmpox
`|- ( x e. A , y e. B |-> C ) = ( z e. A , w e. D |-> E )`

### Proof

Step Hyp Ref Expression
1 cbvmpox.1
` |-  F/_ z B`
2 cbvmpox.2
` |-  F/_ x D`
3 cbvmpox.3
` |-  F/_ z C`
4 cbvmpox.4
` |-  F/_ w C`
5 cbvmpox.5
` |-  F/_ x E`
6 cbvmpox.6
` |-  F/_ y E`
7 cbvmpox.7
` |-  ( x = z -> B = D )`
8 cbvmpox.8
` |-  ( ( x = z /\ y = w ) -> C = E )`
9 nfv
` |-  F/ z x e. A`
10 1 nfcri
` |-  F/ z y e. B`
11 9 10 nfan
` |-  F/ z ( x e. A /\ y e. B )`
12 3 nfeq2
` |-  F/ z u = C`
13 11 12 nfan
` |-  F/ z ( ( x e. A /\ y e. B ) /\ u = C )`
14 nfv
` |-  F/ w x e. A`
15 nfcv
` |-  F/_ w B`
16 15 nfcri
` |-  F/ w y e. B`
17 14 16 nfan
` |-  F/ w ( x e. A /\ y e. B )`
18 4 nfeq2
` |-  F/ w u = C`
19 17 18 nfan
` |-  F/ w ( ( x e. A /\ y e. B ) /\ u = C )`
20 nfv
` |-  F/ x z e. A`
21 2 nfcri
` |-  F/ x w e. D`
22 20 21 nfan
` |-  F/ x ( z e. A /\ w e. D )`
23 5 nfeq2
` |-  F/ x u = E`
24 22 23 nfan
` |-  F/ x ( ( z e. A /\ w e. D ) /\ u = E )`
25 nfv
` |-  F/ y ( z e. A /\ w e. D )`
26 6 nfeq2
` |-  F/ y u = E`
27 25 26 nfan
` |-  F/ y ( ( z e. A /\ w e. D ) /\ u = E )`
28 eleq1w
` |-  ( x = z -> ( x e. A <-> z e. A ) )`
` |-  ( ( x = z /\ y = w ) -> ( x e. A <-> z e. A ) )`
30 7 eleq2d
` |-  ( x = z -> ( y e. B <-> y e. D ) )`
31 eleq1w
` |-  ( y = w -> ( y e. D <-> w e. D ) )`
32 30 31 sylan9bb
` |-  ( ( x = z /\ y = w ) -> ( y e. B <-> w e. D ) )`
33 29 32 anbi12d
` |-  ( ( x = z /\ y = w ) -> ( ( x e. A /\ y e. B ) <-> ( z e. A /\ w e. D ) ) )`
34 8 eqeq2d
` |-  ( ( x = z /\ y = w ) -> ( u = C <-> u = E ) )`
35 33 34 anbi12d
` |-  ( ( x = z /\ y = w ) -> ( ( ( x e. A /\ y e. B ) /\ u = C ) <-> ( ( z e. A /\ w e. D ) /\ u = E ) ) )`
36 13 19 24 27 35 cbvoprab12
` |-  { <. <. x , y >. , u >. | ( ( x e. A /\ y e. B ) /\ u = C ) } = { <. <. z , w >. , u >. | ( ( z e. A /\ w e. D ) /\ u = E ) }`
37 df-mpo
` |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , u >. | ( ( x e. A /\ y e. B ) /\ u = C ) }`
38 df-mpo
` |-  ( z e. A , w e. D |-> E ) = { <. <. z , w >. , u >. | ( ( z e. A /\ w e. D ) /\ u = E ) }`
39 36 37 38 3eqtr4i
` |-  ( x e. A , y e. B |-> C ) = ( z e. A , w e. D |-> E )`