Theorem mpoeq3dv 7448

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ∈ cmpo 7371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-oprab 7373  df-mpo 7374

This theorem is referenced by:  ofeqd  7635  seqomeq12  8399  cantnfval  9597  seqeq2  13946  seqeq3  13947  relexpsucnnr  14967  idfusubc  17842  lsmfval  19552  phssip  21600  mamuval  22313  matsc  22370  marrepval0  22481  marrepval  22482  marepvval0  22486  marepvval  22487  submaval0  22500  mdetr0  22525  mdet0  22526  mdetunilem7  22538  mdetunilem8  22539  madufval  22557  maduval  22558  maducoeval2  22560  madutpos  22562  madugsum  22563  madurid  22564  minmar1val0  22567  minmar1val  22568  pmat0opsc  22618  pmat1opsc  22619  mat2pmatval  22644  cpm2mval  22670  decpmatid  22690  pmatcollpw2lem  22697  pmatcollpw3lem  22703  mply1topmatval  22724  mp2pm2mplem1  22726  mp2pm2mplem4  22729  seqseq123d  28220  ttgval  28855  smatfval  33778  ofceq  34080  reprval  34594  finxpeq1  37367  matunitlindflem1  37603  mnringmulrvald  44209  digfval  48579  2arymaptfv  48633  itcoval  48643  dfswapf2  49243  postcofval  49346  precofval  49349  precofval2  49351  prcofval  49360