Theorem mpteq2dva 4200

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1398   e. wcel 2203   |-> cmpt 4171

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 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-ral 2525  df-opab 4172  df-mpt 4173

This theorem is referenced by:  mpteq2dv  4201  fmptapd  5875  offval  6274  offval2  6282  caofinvl  6292  caofcom  6297  caofdig  6300  freceq1  6623  freceq2  6624  pw2f1odclem  7087  mapxpen  7101  xpmapenlem  7102  2omap  7269  nnnninf2  7418  nninfwlpoimlemginf  7467  fser0const  10897  swrdswrd  11397  sumeq1  12040  sumeq2  12044  prodeq2  12243  prod1dc  12272  restid2  13461  pwsplusgval  13508  pwsmulrval  13509  qusin  13539  prdssgrpd  13628  prdsidlem  13660  prdsmndd  13661  grpinvpropdg  13788  prdsinvlem  13821  pwsinvg  13825  pwssub  13826  mulgrhm2  14758  psrlinv  14839  cnmpt1t  15150  cnmpt12  15152  fsumcncntop  15432  expcn  15434  divccncfap  15455  cdivcncfap  15469  expcncf  15474  divcncfap  15479  maxcncf  15480  mincncf  15481  dvidlemap  15556  dvidrelem  15557  dvidsslem  15558  dvcnp2cntop  15564  dvaddxxbr  15566  dvmulxxbr  15567  dvimulf  15571  dvcoapbr  15572  dvcjbr  15573  dvcj  15574  dvfre  15575  dvexp  15576  dvexp2  15577  dvrecap  15578  dvmptcmulcn  15586  dvmptnegcn  15587  dvmptsubcn  15588  dvmptfsum  15590  dvef  15592  ply1termlem  15607  plypow  15609  plyconst  15610  plyaddlem1  15612  plymullem1  15613  plycolemc  15623  plycjlemc  15625  dvply1  15630  dvply2g  15631  lgsval4lem  15884  lgsneg  15897  lgsmod  15899  lgseisenlem3  15945  lgseisenlem4  15946  pw1map  16769