Theorem mpteq2dva 4134

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1373   e. wcel 2176   |-> cmpt 4105

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-ral 2489  df-opab 4106  df-mpt 4107

This theorem is referenced by:  mpteq2dv  4135  fmptapd  5775  offval  6166  offval2  6174  caofinvl  6184  caofcom  6189  caofdig  6192  freceq1  6478  freceq2  6479  pw2f1odclem  6931  mapxpen  6945  xpmapenlem  6946  nnnninf2  7229  nninfwlpoimlemginf  7278  fser0const  10680  sumeq1  11666  sumeq2  11670  prodeq2  11868  prod1dc  11897  restid2  13080  pwsplusgval  13127  pwsmulrval  13128  qusin  13158  prdssgrpd  13247  prdsidlem  13279  prdsmndd  13280  grpinvpropdg  13407  prdsinvlem  13440  pwsinvg  13444  pwssub  13445  mulgrhm2  14372  psrlinv  14446  cnmpt1t  14757  cnmpt12  14759  fsumcncntop  15039  expcn  15041  divccncfap  15062  cdivcncfap  15076  expcncf  15081  divcncfap  15086  maxcncf  15087  mincncf  15088  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvcnp2cntop  15171  dvaddxxbr  15173  dvmulxxbr  15174  dvimulf  15178  dvcoapbr  15179  dvcjbr  15180  dvcj  15181  dvfre  15182  dvexp  15183  dvexp2  15184  dvrecap  15185  dvmptcmulcn  15193  dvmptnegcn  15194  dvmptsubcn  15195  dvmptfsum  15197  dvef  15199  ply1termlem  15214  plypow  15216  plyconst  15217  plyaddlem1  15219  plymullem1  15220  plycolemc  15230  plycjlemc  15232  dvply1  15237  dvply2g  15238  lgsval4lem  15488  lgsneg  15501  lgsmod  15503  lgseisenlem3  15549  lgseisenlem4  15550  2omap  15932