Theorem mpoeq3dv 7437

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ∈ cmpo 7360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-oprab 7362  df-mpo 7363

This theorem is referenced by:  ofeqd  7624  seqomeq12  8385  cantnfval  9577  seqeq2  13928  seqeq3  13929  relexpsucnnr  14948  idfusubc  17824  lsmfval  19567  phssip  21613  mamuval  22337  matsc  22394  marrepval0  22505  marrepval  22506  marepvval0  22510  marepvval  22511  submaval0  22524  mdetr0  22549  mdet0  22550  mdetunilem7  22562  mdetunilem8  22563  madufval  22581  maduval  22582  maducoeval2  22584  madutpos  22586  madugsum  22587  madurid  22588  minmar1val0  22591  minmar1val  22592  pmat0opsc  22642  pmat1opsc  22643  mat2pmatval  22668  cpm2mval  22694  decpmatid  22714  pmatcollpw2lem  22721  pmatcollpw3lem  22727  mply1topmatval  22748  mp2pm2mplem1  22750  mp2pm2mplem4  22753  seqseq123d  28282  ttgval  28947  smatfval  33952  ofceq  34254  reprval  34767  finxpeq1  37591  matunitlindflem1  37817  mnringmulrvald  44478  digfval  48853  2arymaptfv  48907  itcoval  48917  dfswapf2  49516  postcofval  49619  precofval  49622  precofval2  49624  prcofval  49633