Theorem mpoeq3dv 7529

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108   ∈ cmpo 7450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-oprab 7452  df-mpo 7453

This theorem is referenced by:  ofeqd  7716  seqomeq12  8510  cantnfval  9737  seqeq2  14056  seqeq3  14057  relexpsucnnr  15074  idfusubc  17964  lsmfval  19680  phssip  21699  mamuval  22418  matsc  22477  marrepval0  22588  marrepval  22589  marepvval0  22593  marepvval  22594  submaval0  22607  mdetr0  22632  mdet0  22633  mdetunilem7  22645  mdetunilem8  22646  madufval  22664  maduval  22665  maducoeval2  22667  madutpos  22669  madugsum  22670  madurid  22671  minmar1val0  22674  minmar1val  22675  pmat0opsc  22725  pmat1opsc  22726  mat2pmatval  22751  cpm2mval  22777  decpmatid  22797  pmatcollpw2lem  22804  pmatcollpw3lem  22810  mply1topmatval  22831  mp2pm2mplem1  22833  mp2pm2mplem4  22836  seqseq123d  28310  ttgval  28901  ttgvalOLD  28902  smatfval  33741  ofceq  34061  reprval  34587  finxpeq1  37352  matunitlindflem1  37576  mnringmulrvald  44196  digfval  48331  2arymaptfv  48385  itcoval  48395