Theorem mpteq2dva 4173

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

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

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 4145  df-mpt 4146

This theorem is referenced by:  mpteq2dv  4174  fmptapd  5829  offval  6224  offval2  6232  caofinvl  6242  caofcom  6247  caofdig  6250  freceq1  6536  freceq2  6537  pw2f1odclem  6991  mapxpen  7005  xpmapenlem  7006  nnnninf2  7290  nninfwlpoimlemginf  7339  fser0const  10752  swrdswrd  11232  sumeq1  11861  sumeq2  11865  prodeq2  12063  prod1dc  12092  restid2  13276  pwsplusgval  13323  pwsmulrval  13324  qusin  13354  prdssgrpd  13443  prdsidlem  13475  prdsmndd  13476  grpinvpropdg  13603  prdsinvlem  13636  pwsinvg  13640  pwssub  13641  mulgrhm2  14568  psrlinv  14642  cnmpt1t  14953  cnmpt12  14955  fsumcncntop  15235  expcn  15237  divccncfap  15258  cdivcncfap  15272  expcncf  15277  divcncfap  15282  maxcncf  15283  mincncf  15284  dvidlemap  15359  dvidrelem  15360  dvidsslem  15361  dvcnp2cntop  15367  dvaddxxbr  15369  dvmulxxbr  15370  dvimulf  15374  dvcoapbr  15375  dvcjbr  15376  dvcj  15377  dvfre  15378  dvexp  15379  dvexp2  15380  dvrecap  15381  dvmptcmulcn  15389  dvmptnegcn  15390  dvmptsubcn  15391  dvmptfsum  15393  dvef  15395  ply1termlem  15410  plypow  15412  plyconst  15413  plyaddlem1  15415  plymullem1  15416  plycolemc  15426  plycjlemc  15428  dvply1  15433  dvply2g  15434  lgsval4lem  15684  lgsneg  15697  lgsmod  15699  lgseisenlem3  15745  lgseisenlem4  15746  2omap  16318  pw1map  16320