Metamath Proof Explorer

Theorem cbvmpo1davw2

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

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

Proof

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