Theorem mpteq2dva 4124

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364   ∈ wcel 2167   ↦ cmpt 4095

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-ral 2480  df-opab 4096  df-mpt 4097

This theorem is referenced by:  mpteq2dv  4125  fmptapd  5756  offval  6147  offval2  6155  caofinvl  6165  caofcom  6170  caofdig  6173  freceq1  6459  freceq2  6460  pw2f1odclem  6904  mapxpen  6918  xpmapenlem  6919  nnnninf2  7202  nninfwlpoimlemginf  7251  fser0const  10644  sumeq1  11537  sumeq2  11541  prodeq2  11739  prod1dc  11768  restid2  12950  pwsplusgval  12997  pwsmulrval  12998  qusin  13028  prdssgrpd  13117  prdsidlem  13149  prdsmndd  13150  grpinvpropdg  13277  prdsinvlem  13310  pwsinvg  13314  pwssub  13315  mulgrhm2  14242  psrlinv  14312  cnmpt1t  14605  cnmpt12  14607  fsumcncntop  14887  expcn  14889  divccncfap  14910  cdivcncfap  14924  expcncf  14929  divcncfap  14934  maxcncf  14935  mincncf  14936  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvcnp2cntop  15019  dvaddxxbr  15021  dvmulxxbr  15022  dvimulf  15026  dvcoapbr  15027  dvcjbr  15028  dvcj  15029  dvfre  15030  dvexp  15031  dvexp2  15032  dvrecap  15033  dvmptcmulcn  15041  dvmptnegcn  15042  dvmptsubcn  15043  dvmptfsum  15045  dvef  15047  ply1termlem  15062  plypow  15064  plyconst  15065  plyaddlem1  15067  plymullem1  15068  plycolemc  15078  plycjlemc  15080  dvply1  15085  dvply2g  15086  lgsval4lem  15336  lgsneg  15349  lgsmod  15351  lgseisenlem3  15397  lgseisenlem4  15398  2omap  15726