Theorem mpoeq3dv 7094

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

Syntax hints:   → wi 4   = wceq 1522   ∈ wcel 2080   ∈ cmpo 7021

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-9 2090  ax-12 2140  ax-ext 2768

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1082  df-ex 1763  df-nf 1767  df-sb 2042  df-clab 2775  df-cleq 2787  df-oprab 7023  df-mpo 7024

This theorem is referenced by:  seqomeq12  7944  cantnfval  8980  seqeq2  13223  seqeq3  13224  relexpsucnnr  14218  lsmfval  18493  phssip  20484  mamuval  20679  matsc  20743  marrepval0  20854  marrepval  20855  marepvval0  20859  marepvval  20860  submaval0  20873  mdetr0  20898  mdet0  20899  mdetunilem7  20911  mdetunilem8  20912  madufval  20930  maduval  20931  maducoeval2  20933  madutpos  20935  madugsum  20936  madurid  20937  minmar1val0  20940  minmar1val  20941  pmat0opsc  20990  pmat1opsc  20991  mat2pmatval  21016  cpm2mval  21042  decpmatid  21062  pmatcollpw2lem  21069  pmatcollpw3lem  21075  mply1topmatval  21096  mp2pm2mplem1  21098  mp2pm2mplem4  21101  ttgval  26344  smatfval  30667  ofceq  30965  reprval  31490  finxpeq1  34211  matunitlindflem1  34432  idfusubc  43629  digfval  44152