Theorem mpoeq3dv 7489

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143   ∈ cmpo 7412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-oprab 7414  df-mpo 7415

This theorem is referenced by:  ofeqd  7676  seqomeq12  8437  cantnfval  9633  seqeq2  14037  seqeq3  14038  relexpsucnnr  15058  idfusubc  17952  lsmfval  19703  phssip  21808  mamuval  22550  matsc  22607  marrepval0  22718  marrepval  22719  marepvval0  22723  marepvval  22724  submaval0  22737  mdetr0  22762  mdet0  22763  mdetunilem7  22775  mdetunilem8  22776  madufval  22794  maduval  22795  maducoeval2  22797  madutpos  22799  madugsum  22800  madurid  22801  minmar1val0  22804  minmar1val  22805  pmat0opsc  22855  pmat1opsc  22856  mat2pmatval  22881  cpm2mval  22907  decpmatid  22927  pmatcollpw2lem  22934  pmatcollpw3lem  22940  mply1topmatval  22961  mp2pm2mplem1  22963  mp2pm2mplem4  22966  seqseq123d  28479  ttgval  29224  smatfval  34185  ofceq  34487  reprval  34997  finxpeq1  38052  matunitlindflem1  38287  mnringmulrvald  44971  digfval  49397  2arymaptfv  49451  itcoval  49461  dfswapf2  50059  postcofval  50162  precofval  50165  precofval2  50167  prcofval  50176  crosspdot0i  50664