Theorem mpoeq3dv 7440

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 7438	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ∈ cmpo 7363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-oprab 7365  df-mpo 7366

This theorem is referenced by:  ofeqd  7627  seqomeq12  8387  cantnfval  9583  seqeq2  13961  seqeq3  13962  relexpsucnnr  14981  idfusubc  17861  lsmfval  19607  phssip  21651  mamuval  22371  matsc  22428  marrepval0  22539  marrepval  22540  marepvval0  22544  marepvval  22545  submaval0  22558  mdetr0  22583  mdet0  22584  mdetunilem7  22596  mdetunilem8  22597  madufval  22615  maduval  22616  maducoeval2  22618  madutpos  22620  madugsum  22621  madurid  22622  minmar1val0  22625  minmar1val  22626  pmat0opsc  22676  pmat1opsc  22677  mat2pmatval  22702  cpm2mval  22728  decpmatid  22748  pmatcollpw2lem  22755  pmatcollpw3lem  22761  mply1topmatval  22782  mp2pm2mplem1  22784  mp2pm2mplem4  22787  seqseq123d  28295  ttgval  28960  smatfval  33958  ofceq  34260  reprval  34773  finxpeq1  37719  matunitlindflem1  37954  mnringmulrvald  44675  digfval  49088  2arymaptfv  49142  itcoval  49152  dfswapf2  49751  postcofval  49854  precofval  49857  precofval2  49859  prcofval  49868