Theorem mpteq2dva 4223

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

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

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 4194  df-mpt 4195

This theorem is used by:  mpteq2dv  4224  fmptapd  5909  offval  6314  offval2  6322  caofinvl  6332  caofcom  6337  caofdig  6340  freceq1  6667  freceq2  6668  pw2f1odclem  7138  mapxpen  7152  xpmapenlem  7153  2omap  7324  nnnninf2  7473  nninfwlpoimlemginf  7522  fser0const  10993  swrdswrd  11499  sumeq1  12146  sumeq2  12150  prodeq2  12349  prod1dc  12378  ballotfilemfval  13287  ballotfilemsval  13310  ballotfilemieq  13318  restid2  13661  qusin  13706  grpinvpropdg  13939  gsum2d2fi  14274  prdssgrpd  14298  prdsidlem  14300  prdsmndd  14301  prdsinvlem  14303  pwsplusgval  14315  pwsmulrval  14316  pwsinvg  14322  pwssub  14323  mulgrhm2  15054  asclpropd  15149  psrass1filem  15177  psrlinv  15194  psrass1fi  15201  psrdifi  15202  psrdirfi  15203  cnmpt1t  15511  cnmpt12  15513  fsumcncntop  15793  expcn  15795  divccncfap  15816  cdivcncfap  15830  expcncf  15835  divcncfap  15840  maxcncf  15841  mincncf  15842  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvcnp2cntop  15925  dvaddxxbr  15927  dvmulxxbr  15928  dvimulf  15932  dvcoapbr  15933  dvcjbr  15934  dvcj  15935  dvfre  15936  dvexp  15937  dvexp2  15938  dvrecap  15939  dvmptcmulcn  15947  dvmptnegcn  15948  dvmptsubcn  15949  dvmptfsum  15951  dvef  15953  ply1termlem  15968  plypow  15970  plyconst  15971  plyaddlem1  15973  plymullem1  15974  plycolemc  15984  plycjlemc  15986  dvply1  15991  dvply2g  15992  lgsval4lem  16335  lgsneg  16348  lgsmod  16350  lgseisenlem3  16396  lgseisenlem4  16397  pw1map  17230