Theorem mpoeq3dv 7499

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144   ∈ cmpo 7422

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-oprab 7424  df-mpo 7425

This theorem is used by:  ofeqd  7695  seqomeq12  8465  cantnfval  9670  seqeq2  14149  seqeq3  14150  relexpsucnnr  15179  idfusubc  18076  lsmfval  19853  phssip  21965  mamuval  22709  matsc  22766  marrepval0  22877  marrepval  22878  marepvval0  22882  marepvval  22883  submaval0  22896  mdetr0  22921  mdet0  22922  mdetunilem7  22934  mdetunilem8  22935  madufval  22953  maduval  22954  maducoeval2  22956  madutpos  22958  madugsum  22959  madurid  22960  minmar1val0  22963  minmar1val  22964  matunitlindflem1  22995  pmat0opsc  23017  pmat1opsc  23018  mat2pmatval  23043  cpm2mval  23069  decpmatid  23089  pmatcollpw2lem  23096  pmatcollpw3lem  23102  mply1topmatval  23123  mp2pm2mplem1  23125  mp2pm2mplem4  23128  seqseq123d  28673  ttgval  29453  smatfval  34470  ofceq  34772  reprval  35282  finxpeq1  38385  mnringmulrvald  45301  digfval  49785  2arymaptfv  49839  itcoval  49849  dfswapf2  50445  postcofval  50548  precofval  50551  precofval2  50553  prcofval  50562  crosspdot0lem  51039