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  7319  nnnninf2  7468  nninfwlpoimlemginf  7517  fser0const  10987  swrdswrd  11493  sumeq1  12140  sumeq2  12144  prodeq2  12343  prod1dc  12372  ballotfilemfval  13281  ballotfilemsval  13304  ballotfilemieq  13312  restid2  13655  qusin  13700  grpinvpropdg  13933  prdssgrpd  14275  prdsidlem  14277  prdsmndd  14278  prdsinvlem  14280  pwsplusgval  14292  pwsmulrval  14293  pwsinvg  14299  pwssub  14300  mulgrhm2  15029  asclpropd  15124  psrlinv  15166  cnmpt1t  15477  cnmpt12  15479  fsumcncntop  15759  expcn  15761  divccncfap  15782  cdivcncfap  15796  expcncf  15801  divcncfap  15806  maxcncf  15807  mincncf  15808  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvcnp2cntop  15891  dvaddxxbr  15893  dvmulxxbr  15894  dvimulf  15898  dvcoapbr  15899  dvcjbr  15900  dvcj  15901  dvfre  15902  dvexp  15903  dvexp2  15904  dvrecap  15905  dvmptcmulcn  15913  dvmptnegcn  15914  dvmptsubcn  15915  dvmptfsum  15917  dvef  15919  ply1termlem  15934  plypow  15936  plyconst  15937  plyaddlem1  15939  plymullem1  15940  plycolemc  15950  plycjlemc  15952  dvply1  15957  dvply2g  15958  lgsval4lem  16296  lgsneg  16309  lgsmod  16311  lgseisenlem3  16357  lgseisenlem4  16358  pw1map  17191