Metamath Proof Explorer

Theorem mpt3eqdv

Description: An equality deduction for maps-to notation. (Contributed by BTernaryTau, 8-Sep-2026)

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

Proof

Step Hyp Ref Expression
1 mpt3eqdv.1 
 |-  ( ph -> A = E )
2 mpt3eqdv.2 
 |-  ( ph -> B = F )
3 mpt3eqdv.3 
 |-  ( ph -> C = G )
4 mpt3eqdv.4 
 |-  ( ( ph /\ ( x e. A /\ y e. B /\ z e. C ) ) -> D = H )
5 2 adantr 
 |-  ( ( ph /\ x e. A ) -> B = F )
6 3 3ad2ant1 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> C = G )
7 3an4anass 
 |-  ( ( ( ph /\ x e. A /\ y e. B ) /\ z e. C ) <-> ( ( ph /\ x e. A ) /\ ( y e. B /\ z e. C ) ) )
8 13an22anass 
 |-  ( ( ph /\ ( x e. A /\ y e. B /\ z e. C ) ) <-> ( ( ph /\ x e. A ) /\ ( y e. B /\ z e. C ) ) )
9 7 8 bitr4i 
 |-  ( ( ( ph /\ x e. A /\ y e. B ) /\ z e. C ) <-> ( ph /\ ( x e. A /\ y e. B /\ z e. C ) ) )
10 4 eqeq2d 
 |-  ( ( ph /\ ( x e. A /\ y e. B /\ z e. C ) ) -> ( w = D <-> w = H ) )
11 10 anbi2d 
 |-  ( ( ph /\ ( x e. A /\ y e. B /\ z e. C ) ) -> ( ( v = <. x , y , z >. /\ w = D ) <-> ( v = <. x , y , z >. /\ w = H ) ) )
12 9 11 sylbi 
 |-  ( ( ( ph /\ x e. A /\ y e. B ) /\ z e. C ) -> ( ( v = <. x , y , z >. /\ w = D ) <-> ( v = <. x , y , z >. /\ w = H ) ) )
13 6 12 rexeqbidva 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> ( E. z e. C ( v = <. x , y , z >. /\ w = D ) <-> E. z e. G ( v = <. x , y , z >. /\ w = H ) ) )
14 13 3expa 
 |-  ( ( ( ph /\ x e. A ) /\ y e. B ) -> ( E. z e. C ( v = <. x , y , z >. /\ w = D ) <-> E. z e. G ( v = <. x , y , z >. /\ w = H ) ) )
15 5 14 rexeqbidva 
 |-  ( ( ph /\ x e. A ) -> ( E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) <-> E. y e. F E. z e. G ( v = <. x , y , z >. /\ w = H ) ) )
16 1 15 rexeqbidva 
 |-  ( ph -> ( E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) <-> E. x e. E E. y e. F E. z e. G ( v = <. x , y , z >. /\ w = H ) ) )
17 16 opabbidv 
 |-  ( ph -> { <. v , w >. | E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) } = { <. v , w >. | E. x e. E E. y e. F E. z e. G ( v = <. x , y , z >. /\ w = H ) } )
18 df-mpt3 
 |-  ( x e. A , y e. B , z e. C |-> D ) = { <. v , w >. | E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) }
19 df-mpt3 
 |-  ( x e. E , y e. F , z e. G |-> H ) = { <. v , w >. | E. x e. E E. y e. F E. z e. G ( v = <. x , y , z >. /\ w = H ) }
20 17 18 19 3eqtr4g 
 |-  ( ph -> ( x e. A , y e. B , z e. C |-> D ) = ( x e. E , y e. F , z e. G |-> H ) )