Theorem mpoeq3dv 7471

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-oprab 7394  df-mpo 7395

This theorem is referenced by:  ofeqd  7658  seqomeq12  8425  cantnfval  9628  seqeq2  13977  seqeq3  13978  relexpsucnnr  14998  idfusubc  17869  lsmfval  19575  phssip  21574  mamuval  22287  matsc  22344  marrepval0  22455  marrepval  22456  marepvval0  22460  marepvval  22461  submaval0  22474  mdetr0  22499  mdet0  22500  mdetunilem7  22512  mdetunilem8  22513  madufval  22531  maduval  22532  maducoeval2  22534  madutpos  22536  madugsum  22537  madurid  22538  minmar1val0  22541  minmar1val  22542  pmat0opsc  22592  pmat1opsc  22593  mat2pmatval  22618  cpm2mval  22644  decpmatid  22664  pmatcollpw2lem  22671  pmatcollpw3lem  22677  mply1topmatval  22698  mp2pm2mplem1  22700  mp2pm2mplem4  22703  seqseq123d  28187  ttgval  28809  smatfval  33792  ofceq  34094  reprval  34608  finxpeq1  37381  matunitlindflem1  37617  mnringmulrvald  44223  digfval  48590  2arymaptfv  48644  itcoval  48654  dfswapf2  49254  postcofval  49357  precofval  49360  precofval2  49362  prcofval  49371