Theorem mpoeq3dv 7475

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142   ∈ cmpo 7398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1100  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-oprab 7400  df-mpo 7401

This theorem is referenced by:  ofeqd  7662  seqomeq12  8425  cantnfval  9623  seqeq2  14018  seqeq3  14019  relexpsucnnr  15038  idfusubc  17933  lsmfval  19678  phssip  21710  mamuval  22453  matsc  22510  marrepval0  22621  marrepval  22622  marepvval0  22626  marepvval  22627  submaval0  22640  mdetr0  22665  mdet0  22666  mdetunilem7  22678  mdetunilem8  22679  madufval  22697  maduval  22698  maducoeval2  22700  madutpos  22702  madugsum  22703  madurid  22704  minmar1val0  22707  minmar1val  22708  pmat0opsc  22758  pmat1opsc  22759  mat2pmatval  22784  cpm2mval  22810  decpmatid  22830  pmatcollpw2lem  22837  pmatcollpw3lem  22843  mply1topmatval  22864  mp2pm2mplem1  22866  mp2pm2mplem4  22869  seqseq123d  28379  ttgval  29075  smatfval  34092  ofceq  34394  reprval  34904  finxpeq1  37880  matunitlindflem1  38115  mnringmulrvald  44803  digfval  49219  2arymaptfv  49273  itcoval  49283  dfswapf2  49882  postcofval  49985  precofval  49988  precofval2  49990  prcofval  49999