Theorem mpteq2dva 4216

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1402   e. wcel 2209   |-> cmpt 4187

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-ral 2533  df-opab 4188  df-mpt 4189

This theorem is referenced by:  mpteq2dv  4217  fmptapd  5897  offval  6300  offval2  6308  caofinvl  6318  caofcom  6323  caofdig  6326  freceq1  6653  freceq2  6654  pw2f1odclem  7124  mapxpen  7138  xpmapenlem  7139  2omap  7308  nnnninf2  7457  nninfwlpoimlemginf  7506  fser0const  10950  swrdswrd  11455  sumeq1  12099  sumeq2  12103  prodeq2  12302  prod1dc  12331  ballotfilemfval  13207  ballotfilemsval  13230  ballotfilemieq  13238  restid2  13579  qusin  13624  grpinvpropdg  13857  prdssgrpd  14168  prdsidlem  14170  prdsmndd  14171  prdsinvlem  14173  pwsplusgval  14185  pwsmulrval  14186  pwsinvg  14192  pwssub  14193  mulgrhm2  14917  psrlinv  14998  cnmpt1t  15309  cnmpt12  15311  fsumcncntop  15591  expcn  15593  divccncfap  15614  cdivcncfap  15628  expcncf  15633  divcncfap  15638  maxcncf  15639  mincncf  15640  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dvcnp2cntop  15723  dvaddxxbr  15725  dvmulxxbr  15726  dvimulf  15730  dvcoapbr  15731  dvcjbr  15732  dvcj  15733  dvfre  15734  dvexp  15735  dvexp2  15736  dvrecap  15737  dvmptcmulcn  15745  dvmptnegcn  15746  dvmptsubcn  15747  dvmptfsum  15749  dvef  15751  ply1termlem  15766  plypow  15768  plyconst  15769  plyaddlem1  15771  plymullem1  15772  plycolemc  15782  plycjlemc  15784  dvply1  15789  dvply2g  15790  lgsval4lem  16044  lgsneg  16057  lgsmod  16059  lgseisenlem3  16105  lgseisenlem4  16106  pw1map  16939