Theorem mpteq2dva 4174

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395   ∈ wcel 2200   ↦ cmpt 4145

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-ral 2513  df-opab 4146  df-mpt 4147

This theorem is referenced by:  mpteq2dv  4175  fmptapd  5834  offval  6232  offval2  6240  caofinvl  6250  caofcom  6255  caofdig  6258  freceq1  6544  freceq2  6545  pw2f1odclem  7003  mapxpen  7017  xpmapenlem  7018  nnnninf2  7305  nninfwlpoimlemginf  7354  fser0const  10769  swrdswrd  11252  sumeq1  11881  sumeq2  11885  prodeq2  12083  prod1dc  12112  restid2  13296  pwsplusgval  13343  pwsmulrval  13344  qusin  13374  prdssgrpd  13463  prdsidlem  13495  prdsmndd  13496  grpinvpropdg  13623  prdsinvlem  13656  pwsinvg  13660  pwssub  13661  mulgrhm2  14589  psrlinv  14663  cnmpt1t  14974  cnmpt12  14976  fsumcncntop  15256  expcn  15258  divccncfap  15279  cdivcncfap  15293  expcncf  15298  divcncfap  15303  maxcncf  15304  mincncf  15305  dvidlemap  15380  dvidrelem  15381  dvidsslem  15382  dvcnp2cntop  15388  dvaddxxbr  15390  dvmulxxbr  15391  dvimulf  15395  dvcoapbr  15396  dvcjbr  15397  dvcj  15398  dvfre  15399  dvexp  15400  dvexp2  15401  dvrecap  15402  dvmptcmulcn  15410  dvmptnegcn  15411  dvmptsubcn  15412  dvmptfsum  15414  dvef  15416  ply1termlem  15431  plypow  15433  plyconst  15434  plyaddlem1  15436  plymullem1  15437  plycolemc  15447  plycjlemc  15449  dvply1  15454  dvply2g  15455  lgsval4lem  15705  lgsneg  15718  lgsmod  15720  lgseisenlem3  15766  lgseisenlem4  15767  2omap  16418  pw1map  16420