Theorem mpoeq123dv 7431

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 481	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸)
4		mpoeq123dv.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐹)
5	4	adantr 481	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹)
6	1, 3, 5	mpoeq123dva 7430	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119   ∈ cmpo 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-oprab 7360  df-mpo 7361

This theorem is referenced by:  mpoeq123i  7432  mptmpoopabbrd  8022  el2mpocsbcl  8024  bropopvvv  8029  bropfvvvv  8031  prdsval  17409  imasval  17466  imasvscaval  17493  homffval  17647  homfeq  17651  comfffval  17655  comffval  17656  comfffval2  17658  comffval2  17659  comfeq  17663  oppcval  17670  monfval  17690  sectffval  17708  invffval  17716  isofn  17733  cofuval  17840  natfval  17907  fucval  17919  fucco  17923  coafval  18022  setcval  18035  setcco  18041  catcval  18058  catcco  18063  estrcval  18081  estrcco  18087  xpcval  18134  1stfval  18148  2ndfval  18151  prfval  18156  evlfval  18174  evlf2  18175  curfval  18180  hofval  18209  hof2fval  18212  plusffval  18605  efmnd  18829  grpsubfval  18950  grpsubfvalALT  18951  grpsubpropd  19012  mulgfval  19036  mulgfvalALT  19037  mulgpropd  19083  lsmfval  19604  pj1fval  19660  efgtf  19688  prdsmgp  20123  dvrfval  20373  funcrngcsetcALT  20613  scaffval  20870  ipffval  21623  phssip  21633  frlmip  21753  psrval  21890  mamufval  22375  mvmulfval  22525  marrepfval  22543  marepvfval  22548  submafval  22562  submaval  22564  madufval  22620  minmar1fval  22629  mat2pmatfval  22706  cpm2mfval  22732  decpmatval0  22747  decpmatval  22748  pmatcollpw3lem  22766  xkoval  23570  xkopt  23638  xpstopnlem1  23792  submtmd  24087  blfvalps  24366  ishtpy  24957  isphtpy  24966  pcofval  24995  rrxip  25375  q1pval  26138  r1pval  26141  taylfval  26342  istrkgl  28544  midf  28862  ismidb  28864  ttgval  28961  wwlksnon  29937  wspthsnon  29938  clwwlknonmpo  30177  grpodivfval  30623  dipfval  30791  rlocval  33340  idlsrgval  33586  splyval  33743  submatres  33990  lmatval  33997  lmatcl  34000  qqhval  34156  sxval  34374  sitmval  34533  cndprobval  34617  mclsval  35791  csbfinxpg  37750  rrnval  38194  ldualset  39617  paddfval  40289  tgrpfset  41236  tgrpset  41237  erngfset  41291  erngset  41292  erngfset-rN  41299  erngset-rN  41300  dvafset  41496  dvaset  41497  dvhfset  41572  dvhset  41573  djaffvalN  41625  djafvalN  41626  djhffval  41888  djhfval  41889  hlhilset  42426  eldiophb  43206  mendval  43624  mnringvald  44657  mnringmulrd  44667  hoidmvval  47020  ovnhoi  47046  hspval  47052  hspmbllem2  47070  hoimbl  47074  rngcvalALTV  48756  rngccoALTV  48762  ringcvalALTV  48780  ringccoALTV  48796  lincop  48899  lines  49222  rrxlines  49224  spheres  49237  invfn  49520  infsubc2  49551  imaidfu2  49601  upfval  49666  dfswapf2  49751  swapfval  49752  1stfpropd  49780  2ndfpropd  49781  fucofvalg  49808  fuco21  49826  precofval3  49861  prcofvalg  49866  setc1ocofval  49984  lanfval  50103  ranfval  50104