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 1570   ∈ wcel 2145   ∈ cmpo 7422

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-oprab 7424  df-mpo 7425

This theorem is used by:  ofeqd  7695  seqomeq12  8464  cantnfval  9669  seqeq2  14148  seqeq3  14149  relexpsucnnr  15178  idfusubc  18075  lsmfval  19852  phssip  21964  mamuval  22708  matsc  22765  marrepval0  22876  marrepval  22877  marepvval0  22881  marepvval  22882  submaval0  22895  mdetr0  22920  mdet0  22921  mdetunilem7  22933  mdetunilem8  22934  madufval  22952  maduval  22953  maducoeval2  22955  madutpos  22957  madugsum  22958  madurid  22959  minmar1val0  22962  minmar1val  22963  matunitlindflem1  22994  pmat0opsc  23016  pmat1opsc  23017  mat2pmatval  23042  cpm2mval  23068  decpmatid  23088  pmatcollpw2lem  23095  pmatcollpw3lem  23101  mply1topmatval  23122  mp2pm2mplem1  23124  mp2pm2mplem4  23127  seqseq123d  28672  ttgval  29452  smatfval  34427  ofceq  34729  reprval  35239  finxpeq1  38309  mnringmulrvald  45224  digfval  49708  2arymaptfv  49762  itcoval  49772  dfswapf2  50368  postcofval  50471  precofval  50474  precofval2  50476  prcofval  50485  crosspdot0lem  50962