Theorem mpteq2dva 4184

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 1577	. 2 ⊢ Ⅎ𝑥𝜑
2		mpteq2dva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	1, 2	mpteq2da 4183	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398   ∈ wcel 2202   ↦ cmpt 4155

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-ral 2516  df-opab 4156  df-mpt 4157

This theorem is referenced by:  mpteq2dv  4185  fmptapd  5853  offval  6252  offval2  6260  caofinvl  6270  caofcom  6275  caofdig  6278  freceq1  6601  freceq2  6602  pw2f1odclem  7063  mapxpen  7077  xpmapenlem  7078  nnnninf2  7369  nninfwlpoimlemginf  7418  fser0const  10843  swrdswrd  11335  sumeq1  11978  sumeq2  11982  prodeq2  12181  prod1dc  12210  restid2  13394  pwsplusgval  13441  pwsmulrval  13442  qusin  13472  prdssgrpd  13561  prdsidlem  13593  prdsmndd  13594  grpinvpropdg  13721  prdsinvlem  13754  pwsinvg  13758  pwssub  13759  mulgrhm2  14689  psrlinv  14768  cnmpt1t  15079  cnmpt12  15081  fsumcncntop  15361  expcn  15363  divccncfap  15384  cdivcncfap  15398  expcncf  15403  divcncfap  15408  maxcncf  15409  mincncf  15410  dvidlemap  15485  dvidrelem  15486  dvidsslem  15487  dvcnp2cntop  15493  dvaddxxbr  15495  dvmulxxbr  15496  dvimulf  15500  dvcoapbr  15501  dvcjbr  15502  dvcj  15503  dvfre  15504  dvexp  15505  dvexp2  15506  dvrecap  15507  dvmptcmulcn  15515  dvmptnegcn  15516  dvmptsubcn  15517  dvmptfsum  15519  dvef  15521  ply1termlem  15536  plypow  15538  plyconst  15539  plyaddlem1  15541  plymullem1  15542  plycolemc  15552  plycjlemc  15554  dvply1  15559  dvply2g  15560  lgsval4lem  15813  lgsneg  15826  lgsmod  15828  lgseisenlem3  15874  lgseisenlem4  15875  2omap  16698  pw1map  16700