Theorem mpoeq3dv 7354

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106   ∈ cmpo 7277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-oprab 7279  df-mpo 7280

This theorem is referenced by:  ofeqd  7535  seqomeq12  8285  cantnfval  9426  seqeq2  13725  seqeq3  13726  relexpsucnnr  14736  lsmfval  19243  phssip  20863  mamuval  21535  matsc  21599  marrepval0  21710  marrepval  21711  marepvval0  21715  marepvval  21716  submaval0  21729  mdetr0  21754  mdet0  21755  mdetunilem7  21767  mdetunilem8  21768  madufval  21786  maduval  21787  maducoeval2  21789  madutpos  21791  madugsum  21792  madurid  21793  minmar1val0  21796  minmar1val  21797  pmat0opsc  21847  pmat1opsc  21848  mat2pmatval  21873  cpm2mval  21899  decpmatid  21919  pmatcollpw2lem  21926  pmatcollpw3lem  21932  mply1topmatval  21953  mp2pm2mplem1  21955  mp2pm2mplem4  21958  ttgval  27236  ttgvalOLD  27237  smatfval  31745  ofceq  32065  reprval  32590  finxpeq1  35557  matunitlindflem1  35773  mnringmulrvald  41845  idfusubc  45424  digfval  45943  2arymaptfv  45997  itcoval  46007