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  7318  nnnninf2  7467  nninfwlpoimlemginf  7516  fser0const  10972  swrdswrd  11477  sumeq1  12121  sumeq2  12125  prodeq2  12324  prod1dc  12353  ballotfilemfval  13229  ballotfilemsval  13252  ballotfilemieq  13260  restid2  13602  qusin  13647  grpinvpropdg  13880  prdssgrpd  14191  prdsidlem  14193  prdsmndd  14194  prdsinvlem  14196  pwsplusgval  14208  pwsmulrval  14209  pwsinvg  14215  pwssub  14216  mulgrhm2  14945  asclpropd  15040  psrlinv  15075  cnmpt1t  15386  cnmpt12  15388  fsumcncntop  15668  expcn  15670  divccncfap  15691  cdivcncfap  15705  expcncf  15710  divcncfap  15715  maxcncf  15716  mincncf  15717  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvcnp2cntop  15800  dvaddxxbr  15802  dvmulxxbr  15803  dvimulf  15807  dvcoapbr  15808  dvcjbr  15809  dvcj  15810  dvfre  15811  dvexp  15812  dvexp2  15813  dvrecap  15814  dvmptcmulcn  15822  dvmptnegcn  15823  dvmptsubcn  15824  dvmptfsum  15826  dvef  15828  ply1termlem  15843  plypow  15845  plyconst  15846  plyaddlem1  15848  plymullem1  15849  plycolemc  15859  plycjlemc  15861  dvply1  15866  dvply2g  15867  lgsval4lem  16130  lgsneg  16143  lgsmod  16145  lgseisenlem3  16191  lgseisenlem4  16192  pw1map  17025