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 ) )
29 28 adantr 
 |-  ( ( 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 )