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	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)

Assertion

Ref	Expression
mpteq2dva	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem mpteq2dva

Step	Hyp	Ref	Expression
1		nfv 1576	. 2 ⊢ Ⅎ𝑥𝜑
2		mpteq2dva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	1, 2	mpteq2da 4178	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397   ∈ 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  11920  sumeq2  11924  prodeq2  12123  prod1dc  12152  restid2  13336  pwsplusgval  13383  pwsmulrval  13384  qusin  13414  prdssgrpd  13503  prdsidlem  13535  prdsmndd  13536  grpinvpropdg  13663  prdsinvlem  13696  pwsinvg  13700  pwssub  13701  mulgrhm2  14630  psrlinv  14704  cnmpt1t  15015  cnmpt12  15017  fsumcncntop  15297  expcn  15299  divccncfap  15320  cdivcncfap  15334  expcncf  15339  divcncfap  15344  maxcncf  15345  mincncf  15346  dvidlemap  15421  dvidrelem  15422  dvidsslem  15423  dvcnp2cntop  15429  dvaddxxbr  15431  dvmulxxbr  15432  dvimulf  15436  dvcoapbr  15437  dvcjbr  15438  dvcj  15439  dvfre  15440  dvexp  15441  dvexp2  15442  dvrecap  15443  dvmptcmulcn  15451  dvmptnegcn  15452  dvmptsubcn  15453  dvmptfsum  15455  dvef  15457  ply1termlem  15472  plypow  15474  plyconst  15475  plyaddlem1  15477  plymullem1  15478  plycolemc  15488  plycjlemc  15490  dvply1  15495  dvply2g  15496  lgsval4lem  15746  lgsneg  15759  lgsmod  15761  lgseisenlem3  15807  lgseisenlem4  15808  2omap  16620  pw1map  16622