Theorem mpoeq3dv 7490

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149   ∈ cmpo 7413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-oprab 7415  df-mpo 7416

This theorem is referenced by:  ofeqd  7677  seqomeq12  8440  cantnfval  9636  seqeq2  14040  seqeq3  14041  relexpsucnnr  15061  idfusubc  17956  lsmfval  19707  phssip  21776  mamuval  22518  matsc  22575  marrepval0  22686  marrepval  22687  marepvval0  22691  marepvval  22692  submaval0  22705  mdetr0  22730  mdet0  22731  mdetunilem7  22743  mdetunilem8  22744  madufval  22762  maduval  22763  maducoeval2  22765  madutpos  22767  madugsum  22768  madurid  22769  minmar1val0  22772  minmar1val  22773  pmat0opsc  22823  pmat1opsc  22824  mat2pmatval  22849  cpm2mval  22875  decpmatid  22895  pmatcollpw2lem  22902  pmatcollpw3lem  22908  mply1topmatval  22929  mp2pm2mplem1  22931  mp2pm2mplem4  22934  seqseq123d  28444  ttgval  29164  smatfval  34129  ofceq  34431  reprval  34941  finxpeq1  37919  matunitlindflem1  38154  mnringmulrvald  44842  digfval  49261  2arymaptfv  49315  itcoval  49325  dfswapf2  49923  postcofval  50026  precofval  50029  precofval2  50031  prcofval  50040