Theorem mpoeq3dv 7441

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

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

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 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1089  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-oprab 7366  df-mpo 7367

This theorem is referenced by:  ofeqd  7624  seqomeq12  8405  cantnfval  9613  seqeq2  13920  seqeq3  13921  relexpsucnnr  14922  lsmfval  19434  phssip  21099  mamuval  21772  matsc  21836  marrepval0  21947  marrepval  21948  marepvval0  21952  marepvval  21953  submaval0  21966  mdetr0  21991  mdet0  21992  mdetunilem7  22004  mdetunilem8  22005  madufval  22023  maduval  22024  maducoeval2  22026  madutpos  22028  madugsum  22029  madurid  22030  minmar1val0  22033  minmar1val  22034  pmat0opsc  22084  pmat1opsc  22085  mat2pmatval  22110  cpm2mval  22136  decpmatid  22156  pmatcollpw2lem  22163  pmatcollpw3lem  22169  mply1topmatval  22190  mp2pm2mplem1  22192  mp2pm2mplem4  22195  ttgval  27880  ttgvalOLD  27881  smatfval  32465  ofceq  32785  reprval  33312  finxpeq1  35930  matunitlindflem1  36147  mnringmulrvald  42629  idfusubc  46284  digfval  46803  2arymaptfv  46857  itcoval  46867