Theorem mpoeq3dv 7447

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

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

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 7372  df-mpo 7373

This theorem is referenced by:  ofeqd  7634  seqomeq12  8395  cantnfval  9589  seqeq2  13940  seqeq3  13941  relexpsucnnr  14960  idfusubc  17836  lsmfval  19579  phssip  21625  mamuval  22349  matsc  22406  marrepval0  22517  marrepval  22518  marepvval0  22522  marepvval  22523  submaval0  22536  mdetr0  22561  mdet0  22562  mdetunilem7  22574  mdetunilem8  22575  madufval  22593  maduval  22594  maducoeval2  22596  madutpos  22598  madugsum  22599  madurid  22600  minmar1val0  22603  minmar1val  22604  pmat0opsc  22654  pmat1opsc  22655  mat2pmatval  22680  cpm2mval  22706  decpmatid  22726  pmatcollpw2lem  22733  pmatcollpw3lem  22739  mply1topmatval  22760  mp2pm2mplem1  22762  mp2pm2mplem4  22765  seqseq123d  28294  ttgval  28959  smatfval  33973  ofceq  34275  reprval  34788  finxpeq1  37641  matunitlindflem1  37867  mnringmulrvald  44583  digfval  48957  2arymaptfv  49011  itcoval  49021  dfswapf2  49620  postcofval  49723  precofval  49726  precofval2  49728  prcofval  49737