Theorem mpoeq3dv 7446

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ∈ cmpo 7369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-oprab 7371  df-mpo 7372

This theorem is referenced by:  ofeqd  7633  seqomeq12  8393  cantnfval  9589  seqeq2  13967  seqeq3  13968  relexpsucnnr  14987  idfusubc  17867  lsmfval  19613  phssip  21638  mamuval  22358  matsc  22415  marrepval0  22526  marrepval  22527  marepvval0  22531  marepvval  22532  submaval0  22545  mdetr0  22570  mdet0  22571  mdetunilem7  22583  mdetunilem8  22584  madufval  22602  maduval  22603  maducoeval2  22605  madutpos  22607  madugsum  22608  madurid  22609  minmar1val0  22612  minmar1val  22613  pmat0opsc  22663  pmat1opsc  22664  mat2pmatval  22689  cpm2mval  22715  decpmatid  22735  pmatcollpw2lem  22742  pmatcollpw3lem  22748  mply1topmatval  22769  mp2pm2mplem1  22771  mp2pm2mplem4  22774  seqseq123d  28278  ttgval  28943  smatfval  33939  ofceq  34241  reprval  34754  finxpeq1  37702  matunitlindflem1  37937  mnringmulrvald  44654  digfval  49073  2arymaptfv  49127  itcoval  49137  dfswapf2  49736  postcofval  49839  precofval  49842  precofval2  49844  prcofval  49853