Theorem mpoeq3dv 7493

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ∈ cmpo 7416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-oprab 7418  df-mpo 7419

This theorem is used by:  ofeqd  7681  seqomeq12  8444  cantnfval  9648  seqeq2  14070  seqeq3  14071  relexpsucnnr  15099  idfusubc  17990  lsmfval  19766  phssip  21872  mamuval  22616  matsc  22673  marrepval0  22784  marrepval  22785  marepvval0  22789  marepvval  22790  submaval0  22803  mdetr0  22828  mdet0  22829  mdetunilem7  22841  mdetunilem8  22842  madufval  22860  maduval  22861  maducoeval2  22863  madutpos  22865  madugsum  22866  madurid  22867  minmar1val0  22870  minmar1val  22871  matunitlindflem1  22902  pmat0opsc  22924  pmat1opsc  22925  mat2pmatval  22950  cpm2mval  22976  decpmatid  22996  pmatcollpw2lem  23003  pmatcollpw3lem  23009  mply1topmatval  23030  mp2pm2mplem1  23032  mp2pm2mplem4  23035  seqseq123d  28552  ttgval  29332  smatfval  34306  ofceq  34608  reprval  35119  finxpeq1  38141  mnringmulrvald  45066  digfval  49528  2arymaptfv  49582  itcoval  49592  dfswapf2  50188  postcofval  50291  precofval  50294  precofval2  50296  prcofval  50305  crosspdot0lem  50797