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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ∈ cmpo 7413

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1089  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-oprab 7415  df-mpo 7416

This theorem is referenced by:  ofeqd  7674  seqomeq12  8456  cantnfval  9665  seqeq2  13972  seqeq3  13973  relexpsucnnr  14974  lsmfval  19508  phssip  21217  mamuval  21895  matsc  21959  marrepval0  22070  marrepval  22071  marepvval0  22075  marepvval  22076  submaval0  22089  mdetr0  22114  mdet0  22115  mdetunilem7  22127  mdetunilem8  22128  madufval  22146  maduval  22147  maducoeval2  22149  madutpos  22151  madugsum  22152  madurid  22153  minmar1val0  22156  minmar1val  22157  pmat0opsc  22207  pmat1opsc  22208  mat2pmatval  22233  cpm2mval  22259  decpmatid  22279  pmatcollpw2lem  22286  pmatcollpw3lem  22292  mply1topmatval  22313  mp2pm2mplem1  22315  mp2pm2mplem4  22318  ttgval  28164  ttgvalOLD  28165  smatfval  32844  ofceq  33164  reprval  33691  finxpeq1  36353  matunitlindflem1  36570  mnringmulrvald  43068  idfusubc  46719  digfval  47361  2arymaptfv  47415  itcoval  47425