Theorem mpteq2dva 4177

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

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

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 4149  df-mpt 4150

This theorem is referenced by:  mpteq2dv  4178  fmptapd  5840  offval  6238  offval2  6246  caofinvl  6256  caofcom  6261  caofdig  6264  freceq1  6553  freceq2  6554  pw2f1odclem  7015  mapxpen  7029  xpmapenlem  7030  nnnninf2  7317  nninfwlpoimlemginf  7366  fser0const  10787  swrdswrd  11276  sumeq1  11906  sumeq2  11910  prodeq2  12108  prod1dc  12137  restid2  13321  pwsplusgval  13368  pwsmulrval  13369  qusin  13399  prdssgrpd  13488  prdsidlem  13520  prdsmndd  13521  grpinvpropdg  13648  prdsinvlem  13681  pwsinvg  13685  pwssub  13686  mulgrhm2  14614  psrlinv  14688  cnmpt1t  14999  cnmpt12  15001  fsumcncntop  15281  expcn  15283  divccncfap  15304  cdivcncfap  15318  expcncf  15323  divcncfap  15328  maxcncf  15329  mincncf  15330  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvcnp2cntop  15413  dvaddxxbr  15415  dvmulxxbr  15416  dvimulf  15420  dvcoapbr  15421  dvcjbr  15422  dvcj  15423  dvfre  15424  dvexp  15425  dvexp2  15426  dvrecap  15427  dvmptcmulcn  15435  dvmptnegcn  15436  dvmptsubcn  15437  dvmptfsum  15439  dvef  15441  ply1termlem  15456  plypow  15458  plyconst  15459  plyaddlem1  15461  plymullem1  15462  plycolemc  15472  plycjlemc  15474  dvply1  15479  dvply2g  15480  lgsval4lem  15730  lgsneg  15743  lgsmod  15745  lgseisenlem3  15791  lgseisenlem4  15792  2omap  16530  pw1map  16532