Theorem mpoeq3dv 7511

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105   ∈ cmpo 7432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-oprab 7434  df-mpo 7435

This theorem is referenced by:  ofeqd  7698  seqomeq12  8492  cantnfval  9705  seqeq2  14042  seqeq3  14043  relexpsucnnr  15060  idfusubc  17950  lsmfval  19670  phssip  21693  mamuval  22412  matsc  22471  marrepval0  22582  marrepval  22583  marepvval0  22587  marepvval  22588  submaval0  22601  mdetr0  22626  mdet0  22627  mdetunilem7  22639  mdetunilem8  22640  madufval  22658  maduval  22659  maducoeval2  22661  madutpos  22663  madugsum  22664  madurid  22665  minmar1val0  22668  minmar1val  22669  pmat0opsc  22719  pmat1opsc  22720  mat2pmatval  22745  cpm2mval  22771  decpmatid  22791  pmatcollpw2lem  22798  pmatcollpw3lem  22804  mply1topmatval  22825  mp2pm2mplem1  22827  mp2pm2mplem4  22830  seqseq123d  28306  ttgval  28897  ttgvalOLD  28898  smatfval  33755  ofceq  34077  reprval  34603  finxpeq1  37368  matunitlindflem1  37602  mnringmulrvald  44222  digfval  48446  2arymaptfv  48500  itcoval  48510