Theorem mpoeq3dv 7512

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ∈ cmpo 7433

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-oprab 7435  df-mpo 7436

This theorem is referenced by:  ofeqd  7699  seqomeq12  8494  cantnfval  9708  seqeq2  14046  seqeq3  14047  relexpsucnnr  15064  idfusubc  17945  lsmfval  19656  phssip  21676  mamuval  22397  matsc  22456  marrepval0  22567  marrepval  22568  marepvval0  22572  marepvval  22573  submaval0  22586  mdetr0  22611  mdet0  22612  mdetunilem7  22624  mdetunilem8  22625  madufval  22643  maduval  22644  maducoeval2  22646  madutpos  22648  madugsum  22649  madurid  22650  minmar1val0  22653  minmar1val  22654  pmat0opsc  22704  pmat1opsc  22705  mat2pmatval  22730  cpm2mval  22756  decpmatid  22776  pmatcollpw2lem  22783  pmatcollpw3lem  22789  mply1topmatval  22810  mp2pm2mplem1  22812  mp2pm2mplem4  22815  seqseq123d  28292  ttgval  28883  ttgvalOLD  28884  smatfval  33794  ofceq  34098  reprval  34625  finxpeq1  37387  matunitlindflem1  37623  mnringmulrvald  44246  digfval  48518  2arymaptfv  48572  itcoval  48582  dfswapf2  48967  postcofval  49059  precofval  49062  precofval2  49064