Theorem mpoeq123dv 7487

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2105   ∈ cmpo 7414

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-oprab 7416  df-mpo 7417

This theorem is referenced by:  mpoeq123i  7488  mptmpoopabbrd  8071  mptmpoopabbrdOLD  8073  el2mpocsbcl  8075  bropopvvv  8080  bropfvvvv  8082  prdsval  17406  imasval  17462  imasvscaval  17489  homffval  17639  homfeq  17643  comfffval  17647  comffval  17648  comfffval2  17650  comffval2  17651  comfeq  17655  oppcval  17662  monfval  17684  sectffval  17702  invffval  17710  isofn  17727  cofuval  17837  natfval  17902  fucval  17915  fucco  17920  coafval  18019  setcval  18032  setcco  18038  catcval  18055  catcco  18060  estrcval  18080  estrcco  18086  xpcval  18134  1stfval  18148  2ndfval  18151  prfval  18156  evlfval  18175  evlf2  18176  curfval  18181  hofval  18210  hof2fval  18213  plusffval  18572  efmnd  18788  grpsubfval  18905  grpsubfvalALT  18906  grpsubpropd  18965  mulgfval  18989  mulgfvalALT  18990  mulgpropd  19033  lsmfval  19548  pj1fval  19604  efgtf  19632  prdsmgp  20046  dvrfval  20294  scaffval  20635  ipffval  21421  phssip  21431  frlmip  21553  psrval  21688  mamufval  22108  mvmulfval  22265  marrepfval  22283  marepvfval  22288  submafval  22302  submaval  22304  madufval  22360  minmar1fval  22369  mat2pmatfval  22446  cpm2mfval  22472  decpmatval0  22487  decpmatval  22488  pmatcollpw3lem  22506  xkoval  23312  xkopt  23380  xpstopnlem1  23534  submtmd  23829  blfvalps  24110  ishtpy  24719  isphtpy  24728  pcofval  24758  rrxip  25139  q1pval  25907  r1pval  25910  taylfval  26108  istrkgl  27977  midf  28295  ismidb  28297  ttgval  28394  ttgvalOLD  28395  wwlksnon  29373  wspthsnon  29374  clwwlknonmpo  29610  grpodivfval  30055  dipfval  30223  idlsrgval  32892  submatres  33085  lmatval  33092  lmatcl  33095  qqhval  33253  sxval  33487  sitmval  33647  cndprobval  33731  mclsval  34853  csbfinxpg  36573  rrnval  36999  ldualset  38299  paddfval  38972  tgrpfset  39919  tgrpset  39920  erngfset  39974  erngset  39975  erngfset-rN  39982  erngset-rN  39983  dvafset  40179  dvaset  40180  dvhfset  40255  dvhset  40256  djaffvalN  40308  djafvalN  40309  djhffval  40571  djhfval  40572  hlhilset  41109  eldiophb  41798  mendval  42228  mnringvald  43270  mnringmulrd  43283  hoidmvval  45592  ovnhoi  45618  hspval  45624  hspmbllem2  45642  hoimbl  45646  rngcvalALTV  46948  rngccoALTV  46975  funcrngcsetcALT  46986  ringcvalALTV  46994  ringccoALTV  47038  lincop  47177  lines  47505  rrxlines  47507  spheres  47520