This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Functions in maps-to notation mpteq12dv
Description: An equality inference for the maps-to notation. (Contributed by NM , 24-Aug-2011) (Revised by Mario Carneiro , 16-Dec-2013) Remove
dependency on ax-10 , ax-12 . (Revised by SN and GG , 1-Dec-2023)
Ref
Expression
Hypotheses
mpteq12dv.1 |- ( ph -> A = C )
mpteq12dv.2 |- ( ph -> B = D )
Assertion
mpteq12dv |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Proof
Step
Hyp
Ref
Expression
1
mpteq12dv.1 |- ( ph -> A = C )
2
mpteq12dv.2 |- ( ph -> B = D )
3
2
adantr |- ( ( ph /\ x e. A ) -> B = D )
4
1 3
mpteq12dva |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )