Theorem mpoeq3dv 7486

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ∈ cmpo 7407

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-oprab 7409  df-mpo 7410

This theorem is referenced by:  ofeqd  7673  seqomeq12  8468  cantnfval  9682  seqeq2  14023  seqeq3  14024  relexpsucnnr  15044  idfusubc  17913  lsmfval  19619  phssip  21618  mamuval  22331  matsc  22388  marrepval0  22499  marrepval  22500  marepvval0  22504  marepvval  22505  submaval0  22518  mdetr0  22543  mdet0  22544  mdetunilem7  22556  mdetunilem8  22557  madufval  22575  maduval  22576  maducoeval2  22578  madutpos  22580  madugsum  22581  madurid  22582  minmar1val0  22585  minmar1val  22586  pmat0opsc  22636  pmat1opsc  22637  mat2pmatval  22662  cpm2mval  22688  decpmatid  22708  pmatcollpw2lem  22715  pmatcollpw3lem  22721  mply1topmatval  22742  mp2pm2mplem1  22744  mp2pm2mplem4  22747  seqseq123d  28232  ttgval  28854  smatfval  33826  ofceq  34128  reprval  34642  finxpeq1  37404  matunitlindflem1  37640  mnringmulrvald  44251  digfval  48577  2arymaptfv  48631  itcoval  48641  dfswapf2  49178  postcofval  49275  precofval  49278  precofval2  49280  prcofval  49289