Theorem mpoeq3dv 7332

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108   ∈ cmpo 7257

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-oprab 7259  df-mpo 7260

This theorem is referenced by:  ofeqd  7513  seqomeq12  8255  cantnfval  9356  seqeq2  13653  seqeq3  13654  relexpsucnnr  14664  lsmfval  19158  phssip  20775  mamuval  21445  matsc  21507  marrepval0  21618  marrepval  21619  marepvval0  21623  marepvval  21624  submaval0  21637  mdetr0  21662  mdet0  21663  mdetunilem7  21675  mdetunilem8  21676  madufval  21694  maduval  21695  maducoeval2  21697  madutpos  21699  madugsum  21700  madurid  21701  minmar1val0  21704  minmar1val  21705  pmat0opsc  21755  pmat1opsc  21756  mat2pmatval  21781  cpm2mval  21807  decpmatid  21827  pmatcollpw2lem  21834  pmatcollpw3lem  21840  mply1topmatval  21861  mp2pm2mplem1  21863  mp2pm2mplem4  21866  ttgval  27140  smatfval  31647  ofceq  31965  reprval  32490  finxpeq1  35484  matunitlindflem1  35700  mnringmulrvald  41734  idfusubc  45312  digfval  45831  2arymaptfv  45885  itcoval  45895