Theorem mpteq2dva 4205

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

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

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 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-ral 2527  df-opab 4177  df-mpt 4178

This theorem is referenced by:  mpteq2dv  4206  fmptapd  5880  offval  6283  offval2  6291  caofinvl  6301  caofcom  6306  caofdig  6309  freceq1  6636  freceq2  6637  pw2f1odclem  7100  mapxpen  7114  xpmapenlem  7115  2omap  7282  nnnninf2  7431  nninfwlpoimlemginf  7480  fser0const  10921  swrdswrd  11422  sumeq1  12065  sumeq2  12069  prodeq2  12268  prod1dc  12297  ballotfilemfval  13173  ballotfilemsval  13196  ballotfilemieq  13204  restid2  13545  qusin  13590  grpinvpropdg  13830  prdssgrpd  14133  prdsidlem  14135  prdsmndd  14136  prdsinvlem  14138  pwsplusgval  14150  pwsmulrval  14151  pwsinvg  14157  pwssub  14158  mulgrhm2  14884  psrlinv  14965  cnmpt1t  15276  cnmpt12  15278  fsumcncntop  15558  expcn  15560  divccncfap  15581  cdivcncfap  15595  expcncf  15600  divcncfap  15605  maxcncf  15606  mincncf  15607  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvcnp2cntop  15690  dvaddxxbr  15692  dvmulxxbr  15693  dvimulf  15697  dvcoapbr  15698  dvcjbr  15699  dvcj  15700  dvfre  15701  dvexp  15702  dvexp2  15703  dvrecap  15704  dvmptcmulcn  15712  dvmptnegcn  15713  dvmptsubcn  15714  dvmptfsum  15716  dvef  15718  ply1termlem  15733  plypow  15735  plyconst  15736  plyaddlem1  15738  plymullem1  15739  plycolemc  15749  plycjlemc  15751  dvply1  15756  dvply2g  15757  lgsval4lem  16010  lgsneg  16023  lgsmod  16025  lgseisenlem3  16071  lgseisenlem4  16072  pw1map  16895