Theorem mpoeq3dv 7503

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

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

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 7428  df-mpo 7429

This theorem is used by:  ofeqd  7699  seqomeq12  8472  cantnfval  9676  seqeq2  14155  seqeq3  14156  relexpsucnnr  15187  idfusubc  18084  lsmfval  19861  phssip  21973  mamuval  22717  matsc  22774  marrepval0  22885  marrepval  22886  marepvval0  22890  marepvval  22891  submaval0  22904  mdetr0  22929  mdet0  22930  mdetunilem7  22942  mdetunilem8  22943  madufval  22961  maduval  22962  maducoeval2  22964  madutpos  22966  madugsum  22967  madurid  22968  minmar1val0  22971  minmar1val  22972  matunitlindflem1  23003  pmat0opsc  23025  pmat1opsc  23026  mat2pmatval  23051  cpm2mval  23077  decpmatid  23097  pmatcollpw2lem  23104  pmatcollpw3lem  23110  mply1topmatval  23131  mp2pm2mplem1  23133  mp2pm2mplem4  23136  seqseq123d  28681  ttgval  29461  smatfval  34477  ofceq  34779  reprval  35289  finxpeq1  38446  mnringmulrvald  45362  digfval  49845  2arymaptfv  49899  itcoval  49909  dfswapf2  50519  postcofval  50632  precofval  50638  precofval2  50640  prcofval  50649  crosspdot0lem  51174