Theorem mpoeq3dv 7233

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114   ∈ cmpo 7158

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 1970  ax-7 2015  ax-9 2124  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-oprab 7160  df-mpo 7161

This theorem is referenced by:  seqomeq12  8090  cantnfval  9131  seqeq2  13374  seqeq3  13375  relexpsucnnr  14384  lsmfval  18763  phssip  20802  mamuval  20997  matsc  21059  marrepval0  21170  marrepval  21171  marepvval0  21175  marepvval  21176  submaval0  21189  mdetr0  21214  mdet0  21215  mdetunilem7  21227  mdetunilem8  21228  madufval  21246  maduval  21247  maducoeval2  21249  madutpos  21251  madugsum  21252  madurid  21253  minmar1val0  21256  minmar1val  21257  pmat0opsc  21306  pmat1opsc  21307  mat2pmatval  21332  cpm2mval  21358  decpmatid  21378  pmatcollpw2lem  21385  pmatcollpw3lem  21391  mply1topmatval  21412  mp2pm2mplem1  21414  mp2pm2mplem4  21417  ttgval  26661  smatfval  31060  ofceq  31356  reprval  31881  finxpeq1  34670  matunitlindflem1  34903  idfusubc  44186  digfval  44706