Theorem mpteq2dva 4223

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 4222	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 4193

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 4194  df-mpt 4195

This theorem is used by:  mpteq2dv  4224  fmptapd  5909  offval  6314  offval2  6322  caofinvl  6332  caofcom  6337  caofdig  6340  freceq1  6668  freceq2  6669  pw2f1odclem  7140  mapxpen  7154  xpmapenlem  7155  2omap  7324  nnnninf2  7473  nninfwlpoimlemginf  7522  fser0const  10992  swrdswrd  11498  sumeq1  12145  sumeq2  12149  prodeq2  12348  prod1dc  12377  ballotfilemfval  13286  ballotfilemsval  13309  ballotfilemieq  13317  restid2  13660  qusin  13705  grpinvpropdg  13938  gsum2d2fi  14273  prdssgrpd  14297  prdsidlem  14299  prdsmndd  14300  prdsinvlem  14302  pwsplusgval  14314  pwsmulrval  14315  pwsinvg  14321  pwssub  14322  mulgrhm2  15053  asclpropd  15148  psrass1filem  15186  psrlinv  15203  psrass1fi  15210  psrdifi  15211  psrdirfi  15212  cnmpt1t  15528  cnmpt12  15530  fsumcncntop  15810  expcn  15812  divccncfap  15833  cdivcncfap  15847  expcncf  15852  divcncfap  15857  maxcncf  15858  mincncf  15859  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvcnp2cntop  15942  dvaddxxbr  15944  dvmulxxbr  15945  dvimulf  15949  dvcoapbr  15950  dvcjbr  15951  dvcj  15952  dvfre  15953  dvexp  15954  dvexp2  15955  dvrecap  15956  dvmptcmulcn  15964  dvmptnegcn  15965  dvmptsubcn  15966  dvmptfsum  15968  dvef  15970  ply1termlem  15985  plypow  15987  plyconst  15988  plyaddlem1  15990  plymullem1  15991  plycolemc  16001  plycjlemc  16003  dvply1  16008  dvply2g  16009  lgsval4lem  16352  lgsneg  16365  lgsmod  16367  lgseisenlem3  16413  lgseisenlem4  16414  pw1map  17247