This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mpteq12dva

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017) Remove dependency on ax-10 , ax-12 . (Revised by SN, 11-Nov-2024)

Ref Expression
Hypotheses mpteq12dv.1 
|- ( ph -> A = C )
mpteq12dva.2 
|- ( ( ph /\ x e. A ) -> B = D )
Assertion mpteq12dva 
|- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )

Proof

Step Hyp Ref Expression
1 mpteq12dv.1 
 |-  ( ph -> A = C )
2 mpteq12dva.2 
 |-  ( ( ph /\ x e. A ) -> B = D )
3 2 eqeq2d 
 |-  ( ( ph /\ x e. A ) -> ( y = B <-> y = D ) )
4 3 pm5.32da 
 |-  ( ph -> ( ( x e. A /\ y = B ) <-> ( x e. A /\ y = D ) ) )
5 1 eleq2d 
 |-  ( ph -> ( x e. A <-> x e. C ) )
6 5 anbi1d 
 |-  ( ph -> ( ( x e. A /\ y = D ) <-> ( x e. C /\ y = D ) ) )
7 4 6 bitrd 
 |-  ( ph -> ( ( x e. A /\ y = B ) <-> ( x e. C /\ y = D ) ) )
8 7 opabbidv 
 |-  ( ph -> { <. x , y >. | ( x e. A /\ y = B ) } = { <. x , y >. | ( x e. C /\ y = D ) } )
9 df-mpt 
 |-  ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
10 df-mpt 
 |-  ( x e. C |-> D ) = { <. x , y >. | ( x e. C /\ y = D ) }
11 8 9 10 3eqtr4g 
 |-  ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )