Theorem mpt2eq3dv 6955

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
mpt2eq3dv.1	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
mpt2eq3dv	⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)

Proof of Theorem mpt2eq3dv

Step	Hyp	Ref	Expression
1		mpt2eq3dv.1	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
2	1	3ad2ant1 1164	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)
3	2	mpt2eq3dva 6953	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1653   ∈ wcel 2157   ↦ cmpt2 6880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-oprab 6882  df-mpt2 6883

This theorem is referenced by:  seqomeq12  7788  cantnfval  8815  seqeq2  13059  seqeq3  13060  relexpsucnnr  14106  lsmfval  18366  phssip  20327  mamuval  20517  matsc  20582  marrepval0  20693  marrepval  20694  marepvval0  20698  marepvval  20699  submaval0  20712  mdetr0  20737  mdet0  20738  mdetunilem7  20750  mdetunilem8  20751  madufval  20769  maduval  20770  maducoeval2  20772  madutpos  20774  madugsum  20775  madurid  20776  minmar1val0  20779  minmar1val  20780  pmat0opsc  20831  pmat1opsc  20832  mat2pmatval  20857  cpm2mval  20883  decpmatid  20903  pmatcollpw2lem  20910  pmatcollpw3lem  20916  mply1topmatval  20937  mp2pm2mplem1  20939  mp2pm2mplem4  20942  ttgval  26112  smatfval  30377  ofceq  30675  reprval  31208  finxpeq1  33721  matunitlindflem1  33894  idfusubc  42665  digfval  43190