Theorem mpteq2dva 4221

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 4220	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402   e. wcel 2209   |-> cmpt 4192

This proof depends on 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 proof 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 4193  df-mpt 4194

This theorem is used by:  mpteq2dv  4222  fmptapd  5906  offval  6310  offval2  6318  caofinvl  6328  caofcom  6333  caofdig  6336  freceq1  6663  freceq2  6664  pw2f1odclem  7134  mapxpen  7148  xpmapenlem  7149  2omap  7319  nnnninf2  7468  nninfwlpoimlemginf  7517  fser0const  10987  swrdswrd  11493  sumeq1  12140  sumeq2  12144  prodeq2  12343  prod1dc  12372  ballotfilemfval  13281  ballotfilemsval  13304  ballotfilemieq  13312  restid2  13655  qusin  13700  grpinvpropdg  13933  prdssgrpd  14282  prdsidlem  14284  prdsmndd  14285  prdsinvlem  14287  pwsplusgval  14299  pwsmulrval  14300  pwsinvg  14306  pwssub  14307  mulgrhm2  15036  asclpropd  15131  psrlinv  15173  cnmpt1t  15485  cnmpt12  15487  fsumcncntop  15767  expcn  15769  divccncfap  15790  cdivcncfap  15804  expcncf  15809  divcncfap  15814  maxcncf  15815  mincncf  15816  dvidlemap  15891  dvidrelem  15892  dvidsslem  15893  dvcnp2cntop  15899  dvaddxxbr  15901  dvmulxxbr  15902  dvimulf  15906  dvcoapbr  15907  dvcjbr  15908  dvcj  15909  dvfre  15910  dvexp  15911  dvexp2  15912  dvrecap  15913  dvmptcmulcn  15921  dvmptnegcn  15922  dvmptsubcn  15923  dvmptfsum  15925  dvef  15927  ply1termlem  15942  plypow  15944  plyconst  15945  plyaddlem1  15947  plymullem1  15948  plycolemc  15958  plycjlemc  15960  dvply1  15965  dvply2g  15966  lgsval4lem  16309  lgsneg  16322  lgsmod  16324  lgseisenlem3  16370  lgseisenlem4  16371  pw1map  17204