Theorem mpteq2dva 4124

Description: Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.)

Hypothesis

Ref	Expression
mpteq2dva.1	|- ( ( ph /\ x e. A ) -> B = C )

Assertion

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

Distinct variable group:   ph, x

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

Proof of Theorem mpteq2dva

Step	Hyp	Ref	Expression
1		nfv 1542	. 2 |- F/ x ph
2		mpteq2dva.1	. 2 |- ( ( ph /\ x e. A ) -> B = C )
3	1, 2	mpteq2da 4123	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1364   e. wcel 2167   |-> cmpt 4095

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-ral 2480  df-opab 4096  df-mpt 4097

This theorem is referenced by:  mpteq2dv  4125  fmptapd  5756  offval  6147  offval2  6155  caofinvl  6165  caofcom  6170  caofdig  6173  freceq1  6459  freceq2  6460  pw2f1odclem  6904  mapxpen  6918  xpmapenlem  6919  nnnninf2  7202  nninfwlpoimlemginf  7251  fser0const  10646  sumeq1  11539  sumeq2  11543  prodeq2  11741  prod1dc  11770  restid2  12952  pwsplusgval  12999  pwsmulrval  13000  qusin  13030  prdssgrpd  13119  prdsidlem  13151  prdsmndd  13152  grpinvpropdg  13279  prdsinvlem  13312  pwsinvg  13316  pwssub  13317  mulgrhm2  14244  psrlinv  14318  cnmpt1t  14629  cnmpt12  14631  fsumcncntop  14911  expcn  14913  divccncfap  14934  cdivcncfap  14948  expcncf  14953  divcncfap  14958  maxcncf  14959  mincncf  14960  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvcnp2cntop  15043  dvaddxxbr  15045  dvmulxxbr  15046  dvimulf  15050  dvcoapbr  15051  dvcjbr  15052  dvcj  15053  dvfre  15054  dvexp  15055  dvexp2  15056  dvrecap  15057  dvmptcmulcn  15065  dvmptnegcn  15066  dvmptsubcn  15067  dvmptfsum  15069  dvef  15071  ply1termlem  15086  plypow  15088  plyconst  15089  plyaddlem1  15091  plymullem1  15092  plycolemc  15102  plycjlemc  15104  dvply1  15109  dvply2g  15110  lgsval4lem  15360  lgsneg  15373  lgsmod  15375  lgseisenlem3  15421  lgseisenlem4  15422  2omap  15750