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  11290  sumeq1  11933  sumeq2  11937  prodeq2  12136  prod1dc  12165  restid2  13349  pwsplusgval  13396  pwsmulrval  13397  qusin  13427  prdssgrpd  13516  prdsidlem  13548  prdsmndd  13549  grpinvpropdg  13676  prdsinvlem  13709  pwsinvg  13713  pwssub  13714  mulgrhm2  14643  psrlinv  14717  cnmpt1t  15028  cnmpt12  15030  fsumcncntop  15310  expcn  15312  divccncfap  15333  cdivcncfap  15347  expcncf  15352  divcncfap  15357  maxcncf  15358  mincncf  15359  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvcnp2cntop  15442  dvaddxxbr  15444  dvmulxxbr  15445  dvimulf  15449  dvcoapbr  15450  dvcjbr  15451  dvcj  15452  dvfre  15453  dvexp  15454  dvexp2  15455  dvrecap  15456  dvmptcmulcn  15464  dvmptnegcn  15465  dvmptsubcn  15466  dvmptfsum  15468  dvef  15470  ply1termlem  15485  plypow  15487  plyconst  15488  plyaddlem1  15490  plymullem1  15491  plycolemc  15501  plycjlemc  15503  dvply1  15508  dvply2g  15509  lgsval4lem  15759  lgsneg  15772  lgsmod  15774  lgseisenlem3  15820  lgseisenlem4  15821  2omap  16645  pw1map  16647