Theorem mpoeq3dv 7435

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   ∈ cmpo 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-oprab 7360  df-mpo 7361

This theorem is referenced by:  ofeqd  7622  seqomeq12  8383  cantnfval  9580  seqeq2  13958  seqeq3  13959  relexpsucnnr  14978  idfusubc  17858  lsmfval  19604  phssip  21633  mamuval  22376  matsc  22433  marrepval0  22544  marrepval  22545  marepvval0  22549  marepvval  22550  submaval0  22563  mdetr0  22588  mdet0  22589  mdetunilem7  22601  mdetunilem8  22602  madufval  22620  maduval  22621  maducoeval2  22623  madutpos  22625  madugsum  22626  madurid  22627  minmar1val0  22630  minmar1val  22631  pmat0opsc  22681  pmat1opsc  22682  mat2pmatval  22707  cpm2mval  22733  decpmatid  22753  pmatcollpw2lem  22760  pmatcollpw3lem  22766  mply1topmatval  22787  mp2pm2mplem1  22789  mp2pm2mplem4  22792  seqseq123d  28296  ttgval  28961  smatfval  33979  ofceq  34281  reprval  34794  finxpeq1  37748  matunitlindflem1  37983  mnringmulrvald  44671  digfval  49088  2arymaptfv  49142  itcoval  49152  dfswapf2  49751  postcofval  49854  precofval  49857  precofval2  49859  prcofval  49868