Theorem mpteq12dv 4176

Description: An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.)

Hypotheses

Ref	Expression
mpteq12dv.1	|- ( ph -> A = C )
mpteq12dv.2	|- ( ph -> B = D )

Assertion

Ref	Expression
mpteq12dv	|- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )

Distinct variable group:   ph, x

Allowed substitution hints:   A( x)   B( x)   C( x)   D( x)

Proof of Theorem mpteq12dv

Step	Hyp	Ref	Expression
1		mpteq12dv.1	. 2 |- ( ph -> A = C )
2		mpteq12dv.2	. . 3 |- ( ph -> B = D )
3	2	adantr 276	. 2 |- ( ( ph /\ x e. A ) -> B = D )
4	1, 3	mpteq12dva 4175	1 |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2202   |-> cmpt 4155

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-ral 2516  df-opab 4156  df-mpt 4157

This theorem is referenced by:  mpteq12i  4182  offval  6252  offval3  6305  ccatfvalfi  11235  swrdval  11295  odzval  12894  restval  13408  prdsex  13432  prdsval  13436  qusval  13486  grpinvfvalg  13705  grpinvpropdg  13738  opprnegg  14177  lspfval  14484  lsppropd  14528  sraval  14533  psrval  14762  ntrfval  14911  clsfval  14912  neifval  14951  cnpfval  15006  cnprcl2k  15017  reldvg  15490  dvfvalap  15492  eldvap  15493  vtxdgfval  16229  vtxdgop  16233  vtxdeqd  16237