Theorem mpoeq3dv 7530

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   ∈ cmpo 7453

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-oprab 7455  df-mpo 7456

This theorem is used by:  ofeqd  7727  seqomeq12  8502  cantnfval  9706  seqeq2  14188  seqeq3  14189  relexpsucnnr  15221  idfusubc  18125  lsmfval  19903  phssip  22019  mamuval  22763  matsc  22820  marrepval0  22931  marrepval  22932  marepvval0  22936  marepvval  22937  submaval0  22950  mdetr0  22975  mdet0  22976  mdetunilem7  22988  mdetunilem8  22989  madufval  23007  maduval  23008  maducoeval2  23010  madutpos  23012  madugsum  23013  madurid  23014  minmar1val0  23017  minmar1val  23018  matunitlindflem1  23049  pmat0opsc  23071  pmat1opsc  23072  mat2pmatval  23097  cpm2mval  23123  decpmatid  23143  pmatcollpw2lem  23150  pmatcollpw3lem  23156  mply1topmatval  23177  mp2pm2mplem1  23179  mp2pm2mplem4  23182  seqseq123d  28729  ttgval  29509  smatfval  34538  ofceq  34840  reprval  35350  finxpeq1  38577  mnringmulrvald  45486  digfval  50040  2arymaptfv  50094  itcoval  50104  dfswapf2  50714  postcofval  50827  precofval  50833  precofval2  50835  prcofval  50844  crosspdot0lem  51391