Theorem mpoeq3dv 7290

Description: An equality deduction for the maps-to notation restricted to the value of the operation. (Contributed by SO, 16-Jul-2018.)

Hypothesis

Ref	Expression
mpoeq3dv.1	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
mpoeq3dv	⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)

Proof of Theorem mpoeq3dv

Step	Hyp	Ref	Expression
1		mpoeq3dv.1	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
2	1	3ad2ant1 1135	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)
3	2	mpoeq3dva 7288	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2110   ∈ cmpo 7215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-12 2175  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-oprab 7217  df-mpo 7218

This theorem is referenced by:  seqomeq12  8190  cantnfval  9283  seqeq2  13578  seqeq3  13579  relexpsucnnr  14588  lsmfval  19027  phssip  20620  mamuval  21285  matsc  21347  marrepval0  21458  marrepval  21459  marepvval0  21463  marepvval  21464  submaval0  21477  mdetr0  21502  mdet0  21503  mdetunilem7  21515  mdetunilem8  21516  madufval  21534  maduval  21535  maducoeval2  21537  madutpos  21539  madugsum  21540  madurid  21541  minmar1val0  21544  minmar1val  21545  pmat0opsc  21595  pmat1opsc  21596  mat2pmatval  21621  cpm2mval  21647  decpmatid  21667  pmatcollpw2lem  21674  pmatcollpw3lem  21680  mply1topmatval  21701  mp2pm2mplem1  21703  mp2pm2mplem4  21706  ttgval  26966  smatfval  31459  ofceq  31777  reprval  32302  finxpeq1  35294  matunitlindflem1  35510  mnringmulrvald  41518  idfusubc  45097  digfval  45616  2arymaptfv  45670  itcoval  45680