Theorem mpteq2dva 4221

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   = wceq 1402   ∈ wcel 2209   ↦ cmpt 4192

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-ral 2533  df-opab 4193  df-mpt 4194

This theorem is used by:  mpteq2dv  4222  fmptapd  5906  offval  6310  offval2  6318  caofinvl  6328  caofcom  6333  caofdig  6336  freceq1  6663  freceq2  6664  pw2f1odclem  7134  mapxpen  7148  xpmapenlem  7149  2omap  7318  nnnninf2  7467  nninfwlpoimlemginf  7516  fser0const  10985  swrdswrd  11491  sumeq1  12137  sumeq2  12141  prodeq2  12340  prod1dc  12369  ballotfilemfval  13278  ballotfilemsval  13301  ballotfilemieq  13309  restid2  13651  qusin  13696  grpinvpropdg  13929  prdssgrpd  14240  prdsidlem  14242  prdsmndd  14243  prdsinvlem  14245  pwsplusgval  14257  pwsmulrval  14258  pwsinvg  14264  pwssub  14265  mulgrhm2  14994  asclpropd  15089  psrlinv  15124  cnmpt1t  15435  cnmpt12  15437  fsumcncntop  15717  expcn  15719  divccncfap  15740  cdivcncfap  15754  expcncf  15759  divcncfap  15764  maxcncf  15765  mincncf  15766  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvcnp2cntop  15849  dvaddxxbr  15851  dvmulxxbr  15852  dvimulf  15856  dvcoapbr  15857  dvcjbr  15858  dvcj  15859  dvfre  15860  dvexp  15861  dvexp2  15862  dvrecap  15863  dvmptcmulcn  15871  dvmptnegcn  15872  dvmptsubcn  15873  dvmptfsum  15875  dvef  15877  ply1termlem  15892  plypow  15894  plyconst  15895  plyaddlem1  15897  plymullem1  15898  plycolemc  15908  plycjlemc  15910  dvply1  15915  dvply2g  15916  lgsval4lem  16228  lgsneg  16241  lgsmod  16243  lgseisenlem3  16289  lgseisenlem4  16290  pw1map  17123