Theorem mpoeq123dv 7509

Description: An equality deduction for the maps-to notation. (Contributed by NM, 12-Sep-2011.)

Hypotheses

Ref	Expression
mpoeq123dv.1	⊢ (𝜑 → 𝐴 = 𝐷)
mpoeq123dv.2	⊢ (𝜑 → 𝐵 = 𝐸)
mpoeq123dv.3	⊢ (𝜑 → 𝐶 = 𝐹)

Assertion

Ref	Expression
mpoeq123dv	⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)   𝐸(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem mpoeq123dv

Step	Hyp	Ref	Expression
1		mpoeq123dv.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐷)
2		mpoeq123dv.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐸)
3	2	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸)
4		mpoeq123dv.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐹)
5	4	adantr 480	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹)
6	1, 3, 5	mpoeq123dva 7508	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107   ∈ cmpo 7434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-oprab 7436  df-mpo 7437

This theorem is referenced by:  mpoeq123i  7510  mptmpoopabbrd  8106  mptmpoopabbrdOLD  8107  mptmpoopabbrdOLDOLD  8109  el2mpocsbcl  8111  bropopvvv  8116  bropfvvvv  8118  prdsval  17501  imasval  17557  imasvscaval  17584  homffval  17734  homfeq  17738  comfffval  17742  comffval  17743  comfffval2  17745  comffval2  17746  comfeq  17750  oppcval  17757  monfval  17777  sectffval  17795  invffval  17803  isofn  17820  cofuval  17928  natfval  17995  fucval  18007  fucco  18011  coafval  18110  setcval  18123  setcco  18129  catcval  18146  catcco  18151  estrcval  18169  estrcco  18175  xpcval  18223  1stfval  18237  2ndfval  18240  prfval  18245  evlfval  18263  evlf2  18264  curfval  18269  hofval  18298  hof2fval  18301  plusffval  18660  efmnd  18884  grpsubfval  19002  grpsubfvalALT  19003  grpsubpropd  19064  mulgfval  19088  mulgfvalALT  19089  mulgpropd  19135  lsmfval  19657  pj1fval  19713  efgtf  19741  prdsmgp  20149  dvrfval  20403  funcrngcsetcALT  20642  scaffval  20879  ipffval  21667  phssip  21677  frlmip  21799  psrval  21936  mamufval  22397  mvmulfval  22549  marrepfval  22567  marepvfval  22572  submafval  22586  submaval  22588  madufval  22644  minmar1fval  22653  mat2pmatfval  22730  cpm2mfval  22756  decpmatval0  22771  decpmatval  22772  pmatcollpw3lem  22790  xkoval  23596  xkopt  23664  xpstopnlem1  23818  submtmd  24113  blfvalps  24394  ishtpy  25005  isphtpy  25014  pcofval  25044  rrxip  25425  q1pval  26195  r1pval  26198  taylfval  26401  istrkgl  28467  midf  28785  ismidb  28787  ttgval  28884  ttgvalOLD  28885  wwlksnon  29872  wspthsnon  29873  clwwlknonmpo  30109  grpodivfval  30554  dipfval  30722  rlocval  33264  idlsrgval  33532  submatres  33806  lmatval  33813  lmatcl  33816  qqhval  33974  sxval  34192  sitmval  34352  cndprobval  34436  mclsval  35569  csbfinxpg  37390  rrnval  37835  ldualset  39127  paddfval  39800  tgrpfset  40747  tgrpset  40748  erngfset  40802  erngset  40803  erngfset-rN  40810  erngset-rN  40811  dvafset  41007  dvaset  41008  dvhfset  41083  dvhset  41084  djaffvalN  41136  djafvalN  41137  djhffval  41399  djhfval  41400  hlhilset  41937  eldiophb  42773  mendval  43196  mnringvald  44232  mnringmulrd  44245  hoidmvval  46597  ovnhoi  46623  hspval  46629  hspmbllem2  46647  hoimbl  46651  rngcvalALTV  48186  rngccoALTV  48192  ringcvalALTV  48210  ringccoALTV  48226  lincop  48330  lines  48657  rrxlines  48659  spheres  48672  upfval  48951  dfswapf2  48985  swapfval  48986  fucofvalg  49036  fuco21  49054  precofval3  49089