Theorem mpoeq3dv 7488

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 1134	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)
3	2	mpoeq3dva 7486	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107   ∈ cmpo 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-oprab 7413  df-mpo 7414

This theorem is referenced by:  ofeqd  7672  seqomeq12  8454  cantnfval  9663  seqeq2  13970  seqeq3  13971  relexpsucnnr  14972  lsmfval  19506  phssip  21211  mamuval  21888  matsc  21952  marrepval0  22063  marrepval  22064  marepvval0  22068  marepvval  22069  submaval0  22082  mdetr0  22107  mdet0  22108  mdetunilem7  22120  mdetunilem8  22121  madufval  22139  maduval  22140  maducoeval2  22142  madutpos  22144  madugsum  22145  madurid  22146  minmar1val0  22149  minmar1val  22150  pmat0opsc  22200  pmat1opsc  22201  mat2pmatval  22226  cpm2mval  22252  decpmatid  22272  pmatcollpw2lem  22279  pmatcollpw3lem  22285  mply1topmatval  22306  mp2pm2mplem1  22308  mp2pm2mplem4  22311  ttgval  28126  ttgvalOLD  28127  smatfval  32775  ofceq  33095  reprval  33622  finxpeq1  36267  matunitlindflem1  36484  mnringmulrvald  42986  idfusubc  46640  digfval  47283  2arymaptfv  47337  itcoval  47347