Metamath Proof Explorer

Theorem cbvmpodavw2

Description: Change bound variable and domains in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025)

Ref Expression
Hypotheses cbvmpodavw2.1 
|- ( ( ( ph /\ x = z ) /\ y = w ) -> E = F )
cbvmpodavw2.2 
|- ( ( ( ph /\ x = z ) /\ y = w ) -> C = D )
cbvmpodavw2.3 
|- ( ( ( ph /\ x = z ) /\ y = w ) -> A = B )
Assertion cbvmpodavw2 
|- ( ph -> ( x e. A , y e. C |-> E ) = ( z e. B , w e. D |-> F ) )

Proof

Step Hyp Ref Expression
1 cbvmpodavw2.1 
 |-  ( ( ( ph /\ x = z ) /\ y = w ) -> E = F )
2 cbvmpodavw2.2 
 |-  ( ( ( ph /\ x = z ) /\ y = w ) -> C = D )
3 cbvmpodavw2.3 
 |-  ( ( ( ph /\ x = z ) /\ y = w ) -> A = B )
4 simplr 
 |-  ( ( ( ph /\ x = z ) /\ y = w ) -> x = z )
5 4 3 eleq12d 
 |-  ( ( ( ph /\ x = z ) /\ y = w ) -> ( x e. A <-> z e. B ) )
6 simpr 
 |-  ( ( ( ph /\ x = z ) /\ y = w ) -> y = w )
7 6 2 eleq12d 
 |-  ( ( ( ph /\ x = z ) /\ y = w ) -> ( y e. C <-> w e. D ) )
8 5 7 anbi12d 
 |-  ( ( ( ph /\ x = z ) /\ y = w ) -> ( ( x e. A /\ y e. C ) <-> ( z e. B /\ w e. D ) ) )
9 1 eqeq2d 
 |-  ( ( ( ph /\ x = z ) /\ y = w ) -> ( t = E <-> t = F ) )
10 8 9 anbi12d 
 |-  ( ( ( ph /\ x = z ) /\ y = w ) -> ( ( ( x e. A /\ y e. C ) /\ t = E ) <-> ( ( z e. B /\ w e. D ) /\ t = F ) ) )
11 10 cbvoprab12davw 
 |-  ( ph -> { <. <. x , y >. , t >. | ( ( x e. A /\ y e. C ) /\ t = E ) } = { <. <. z , w >. , t >. | ( ( z e. B /\ w e. D ) /\ t = F ) } )
12 df-mpo 
 |-  ( x e. A , y e. C |-> E ) = { <. <. x , y >. , t >. | ( ( x e. A /\ y e. C ) /\ t = E ) }
13 df-mpo 
 |-  ( z e. B , w e. D |-> F ) = { <. <. z , w >. , t >. | ( ( z e. B /\ w e. D ) /\ t = F ) }
14 11 12 13 3eqtr4g 
 |-  ( ph -> ( x e. A , y e. C |-> E ) = ( z e. B , w e. D |-> F ) )