Theorem mpteq2dva 4141

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1373   ∈ wcel 2177   ↦ cmpt 4112

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-ral 2490  df-opab 4113  df-mpt 4114

This theorem is referenced by:  mpteq2dv  4142  fmptapd  5787  offval  6178  offval2  6186  caofinvl  6196  caofcom  6201  caofdig  6204  freceq1  6490  freceq2  6491  pw2f1odclem  6945  mapxpen  6959  xpmapenlem  6960  nnnninf2  7243  nninfwlpoimlemginf  7292  fser0const  10697  swrdswrd  11176  sumeq1  11736  sumeq2  11740  prodeq2  11938  prod1dc  11967  restid2  13150  pwsplusgval  13197  pwsmulrval  13198  qusin  13228  prdssgrpd  13317  prdsidlem  13349  prdsmndd  13350  grpinvpropdg  13477  prdsinvlem  13510  pwsinvg  13514  pwssub  13515  mulgrhm2  14442  psrlinv  14516  cnmpt1t  14827  cnmpt12  14829  fsumcncntop  15109  expcn  15111  divccncfap  15132  cdivcncfap  15146  expcncf  15151  divcncfap  15156  maxcncf  15157  mincncf  15158  dvidlemap  15233  dvidrelem  15234  dvidsslem  15235  dvcnp2cntop  15241  dvaddxxbr  15243  dvmulxxbr  15244  dvimulf  15248  dvcoapbr  15249  dvcjbr  15250  dvcj  15251  dvfre  15252  dvexp  15253  dvexp2  15254  dvrecap  15255  dvmptcmulcn  15263  dvmptnegcn  15264  dvmptsubcn  15265  dvmptfsum  15267  dvef  15269  ply1termlem  15284  plypow  15286  plyconst  15287  plyaddlem1  15289  plymullem1  15290  plycolemc  15300  plycjlemc  15302  dvply1  15307  dvply2g  15308  lgsval4lem  15558  lgsneg  15571  lgsmod  15573  lgseisenlem3  15619  lgseisenlem4  15620  2omap  16067