Theorem mpteq2dva 4133

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 1550	. 2 |- F/ x ph
2		mpteq2dva.1	. 2 |- ( ( ph /\ x e. A ) -> B = C )
3	1, 2	mpteq2da 4132	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1372   e. wcel 2175   |-> cmpt 4104

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-ral 2488  df-opab 4105  df-mpt 4106

This theorem is referenced by:  mpteq2dv  4134  fmptapd  5774  offval  6165  offval2  6173  caofinvl  6183  caofcom  6188  caofdig  6191  freceq1  6477  freceq2  6478  pw2f1odclem  6930  mapxpen  6944  xpmapenlem  6945  nnnninf2  7228  nninfwlpoimlemginf  7277  fser0const  10678  sumeq1  11637  sumeq2  11641  prodeq2  11839  prod1dc  11868  restid2  13051  pwsplusgval  13098  pwsmulrval  13099  qusin  13129  prdssgrpd  13218  prdsidlem  13250  prdsmndd  13251  grpinvpropdg  13378  prdsinvlem  13411  pwsinvg  13415  pwssub  13416  mulgrhm2  14343  psrlinv  14417  cnmpt1t  14728  cnmpt12  14730  fsumcncntop  15010  expcn  15012  divccncfap  15033  cdivcncfap  15047  expcncf  15052  divcncfap  15057  maxcncf  15058  mincncf  15059  dvidlemap  15134  dvidrelem  15135  dvidsslem  15136  dvcnp2cntop  15142  dvaddxxbr  15144  dvmulxxbr  15145  dvimulf  15149  dvcoapbr  15150  dvcjbr  15151  dvcj  15152  dvfre  15153  dvexp  15154  dvexp2  15155  dvrecap  15156  dvmptcmulcn  15164  dvmptnegcn  15165  dvmptsubcn  15166  dvmptfsum  15168  dvef  15170  ply1termlem  15185  plypow  15187  plyconst  15188  plyaddlem1  15190  plymullem1  15191  plycolemc  15201  plycjlemc  15203  dvply1  15208  dvply2g  15209  lgsval4lem  15459  lgsneg  15472  lgsmod  15474  lgseisenlem3  15520  lgseisenlem4  15521  2omap  15894