Theorem mpoeq3dv 7425

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111   ∈ cmpo 7348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-oprab 7350  df-mpo 7351

This theorem is referenced by:  ofeqd  7612  seqomeq12  8373  cantnfval  9558  seqeq2  13912  seqeq3  13913  relexpsucnnr  14932  idfusubc  17807  lsmfval  19550  phssip  21595  mamuval  22308  matsc  22365  marrepval0  22476  marrepval  22477  marepvval0  22481  marepvval  22482  submaval0  22495  mdetr0  22520  mdet0  22521  mdetunilem7  22533  mdetunilem8  22534  madufval  22552  maduval  22553  maducoeval2  22555  madutpos  22557  madugsum  22558  madurid  22559  minmar1val0  22562  minmar1val  22563  pmat0opsc  22613  pmat1opsc  22614  mat2pmatval  22639  cpm2mval  22665  decpmatid  22685  pmatcollpw2lem  22692  pmatcollpw3lem  22698  mply1topmatval  22719  mp2pm2mplem1  22721  mp2pm2mplem4  22724  seqseq123d  28216  ttgval  28853  smatfval  33808  ofceq  34110  reprval  34623  finxpeq1  37430  matunitlindflem1  37666  mnringmulrvald  44330  digfval  48708  2arymaptfv  48762  itcoval  48772  dfswapf2  49372  postcofval  49475  precofval  49478  precofval2  49480  prcofval  49489