Theorem mpoeq3dv 7468

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

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

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 7391  df-mpo 7392

This theorem is referenced by:  ofeqd  7655  seqomeq12  8422  cantnfval  9621  seqeq2  13970  seqeq3  13971  relexpsucnnr  14991  idfusubc  17862  lsmfval  19568  phssip  21567  mamuval  22280  matsc  22337  marrepval0  22448  marrepval  22449  marepvval0  22453  marepvval  22454  submaval0  22467  mdetr0  22492  mdet0  22493  mdetunilem7  22505  mdetunilem8  22506  madufval  22524  maduval  22525  maducoeval2  22527  madutpos  22529  madugsum  22530  madurid  22531  minmar1val0  22534  minmar1val  22535  pmat0opsc  22585  pmat1opsc  22586  mat2pmatval  22611  cpm2mval  22637  decpmatid  22657  pmatcollpw2lem  22664  pmatcollpw3lem  22670  mply1topmatval  22691  mp2pm2mplem1  22693  mp2pm2mplem4  22696  seqseq123d  28180  ttgval  28802  smatfval  33785  ofceq  34087  reprval  34601  finxpeq1  37374  matunitlindflem1  37610  mnringmulrvald  44216  digfval  48586  2arymaptfv  48640  itcoval  48650  dfswapf2  49250  postcofval  49353  precofval  49356  precofval2  49358  prcofval  49367