Theorem mpoeq3dv 7428

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

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

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 7353  df-mpo 7354

This theorem is referenced by:  ofeqd  7615  seqomeq12  8376  cantnfval  9564  seqeq2  13912  seqeq3  13913  relexpsucnnr  14932  idfusubc  17807  lsmfval  19517  phssip  21565  mamuval  22278  matsc  22335  marrepval0  22446  marrepval  22447  marepvval0  22451  marepvval  22452  submaval0  22465  mdetr0  22490  mdet0  22491  mdetunilem7  22503  mdetunilem8  22504  madufval  22522  maduval  22523  maducoeval2  22525  madutpos  22527  madugsum  22528  madurid  22529  minmar1val0  22532  minmar1val  22533  pmat0opsc  22583  pmat1opsc  22584  mat2pmatval  22609  cpm2mval  22635  decpmatid  22655  pmatcollpw2lem  22662  pmatcollpw3lem  22668  mply1topmatval  22689  mp2pm2mplem1  22691  mp2pm2mplem4  22694  seqseq123d  28185  ttgval  28820  smatfval  33762  ofceq  34064  reprval  34578  finxpeq1  37364  matunitlindflem1  37600  mnringmulrvald  44204  digfval  48586  2arymaptfv  48640  itcoval  48650  dfswapf2  49250  postcofval  49353  precofval  49356  precofval2  49358  prcofval  49367