Theorem mpoeq3dv 7491

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105   ∈ cmpo 7414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1088  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-oprab 7416  df-mpo 7417

This theorem is referenced by:  ofeqd  7676  seqomeq12  8460  cantnfval  9669  seqeq2  13977  seqeq3  13978  relexpsucnnr  14979  idfusubc  17857  lsmfval  19554  phssip  21520  mamuval  22207  matsc  22271  marrepval0  22382  marrepval  22383  marepvval0  22387  marepvval  22388  submaval0  22401  mdetr0  22426  mdet0  22427  mdetunilem7  22439  mdetunilem8  22440  madufval  22458  maduval  22459  maducoeval2  22461  madutpos  22463  madugsum  22464  madurid  22465  minmar1val0  22468  minmar1val  22469  pmat0opsc  22519  pmat1opsc  22520  mat2pmatval  22545  cpm2mval  22571  decpmatid  22591  pmatcollpw2lem  22598  pmatcollpw3lem  22604  mply1topmatval  22625  mp2pm2mplem1  22627  mp2pm2mplem4  22630  ttgval  28558  ttgvalOLD  28559  smatfval  33238  ofceq  33558  reprval  34085  finxpeq1  36730  matunitlindflem1  36947  mnringmulrvald  43448  digfval  47444  2arymaptfv  47498  itcoval  47508