Theorem mpteq2dva 4179

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1397   e. wcel 2202   |-> cmpt 4150

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-ral 2515  df-opab 4151  df-mpt 4152

This theorem is referenced by:  mpteq2dv  4180  fmptapd  5845  offval  6243  offval2  6251  caofinvl  6261  caofcom  6266  caofdig  6269  freceq1  6558  freceq2  6559  pw2f1odclem  7020  mapxpen  7034  xpmapenlem  7035  nnnninf2  7326  nninfwlpoimlemginf  7375  fser0const  10798  swrdswrd  11287  sumeq1  11917  sumeq2  11921  prodeq2  12120  prod1dc  12149  restid2  13333  pwsplusgval  13380  pwsmulrval  13381  qusin  13411  prdssgrpd  13500  prdsidlem  13532  prdsmndd  13533  grpinvpropdg  13660  prdsinvlem  13693  pwsinvg  13697  pwssub  13698  mulgrhm2  14627  psrlinv  14701  cnmpt1t  15012  cnmpt12  15014  fsumcncntop  15294  expcn  15296  divccncfap  15317  cdivcncfap  15331  expcncf  15336  divcncfap  15341  maxcncf  15342  mincncf  15343  dvidlemap  15418  dvidrelem  15419  dvidsslem  15420  dvcnp2cntop  15426  dvaddxxbr  15428  dvmulxxbr  15429  dvimulf  15433  dvcoapbr  15434  dvcjbr  15435  dvcj  15436  dvfre  15437  dvexp  15438  dvexp2  15439  dvrecap  15440  dvmptcmulcn  15448  dvmptnegcn  15449  dvmptsubcn  15450  dvmptfsum  15452  dvef  15454  ply1termlem  15469  plypow  15471  plyconst  15472  plyaddlem1  15474  plymullem1  15475  plycolemc  15485  plycjlemc  15487  dvply1  15492  dvply2g  15493  lgsval4lem  15743  lgsneg  15756  lgsmod  15758  lgseisenlem3  15804  lgseisenlem4  15805  2omap  16611  pw1map  16613