Theorem mpoeq3dv 7435

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ∈ cmpo 7358

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 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-oprab 7360  df-mpo 7361

This theorem is referenced by:  ofeqd  7622  seqomeq12  8383  cantnfval  9575  seqeq2  13926  seqeq3  13927  relexpsucnnr  14946  idfusubc  17822  lsmfval  19565  phssip  21611  mamuval  22335  matsc  22392  marrepval0  22503  marrepval  22504  marepvval0  22508  marepvval  22509  submaval0  22522  mdetr0  22547  mdet0  22548  mdetunilem7  22560  mdetunilem8  22561  madufval  22579  maduval  22580  maducoeval2  22582  madutpos  22584  madugsum  22585  madurid  22586  minmar1val0  22589  minmar1val  22590  pmat0opsc  22640  pmat1opsc  22641  mat2pmatval  22666  cpm2mval  22692  decpmatid  22712  pmatcollpw2lem  22719  pmatcollpw3lem  22725  mply1topmatval  22746  mp2pm2mplem1  22748  mp2pm2mplem4  22751  seqseq123d  28247  ttgval  28896  smatfval  33901  ofceq  34203  reprval  34716  finxpeq1  37530  matunitlindflem1  37756  mnringmulrvald  44410  digfval  48785  2arymaptfv  48839  itcoval  48849  dfswapf2  49448  postcofval  49551  precofval  49554  precofval2  49556  prcofval  49565