Theorem mpoeq3dv 7498

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   ∈ cmpo 7421

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 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-oprab 7423  df-mpo 7424

This theorem is used by:  ofeqd  7686  seqomeq12  8447  cantnfval  9644  seqeq2  14061  seqeq3  14062  relexpsucnnr  15088  idfusubc  17981  lsmfval  19754  phssip  21860  mamuval  22602  matsc  22659  marrepval0  22770  marrepval  22771  marepvval0  22775  marepvval  22776  submaval0  22789  mdetr0  22814  mdet0  22815  mdetunilem7  22827  mdetunilem8  22828  madufval  22846  maduval  22847  maducoeval2  22849  madutpos  22851  madugsum  22852  madurid  22853  minmar1val0  22856  minmar1val  22857  pmat0opsc  22907  pmat1opsc  22908  mat2pmatval  22933  cpm2mval  22959  decpmatid  22979  pmatcollpw2lem  22986  pmatcollpw3lem  22992  mply1topmatval  23013  mp2pm2mplem1  23015  mp2pm2mplem4  23018  seqseq123d  28532  ttgval  29281  smatfval  34251  ofceq  34553  reprval  35064  finxpeq1  38091  matunitlindflem1  38326  mnringmulrvald  45011  digfval  49436  2arymaptfv  49490  itcoval  49500  dfswapf2  50098  postcofval  50201  precofval  50204  precofval2  50206  prcofval  50215  crosspdot0lem  50704