Theorem mpoeq123dv 7485

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

Syntax hints:   → wi 4   ∧ wa 400   = 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-8 2145  ax-9 2153  ax-ext 2735

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

This theorem is referenced by:  mpoeq123i  7486  mptmpoopabbrd  8074  el2mpocsbcl  8076  bropopvvv  8081  bropfvvvv  8083  prdsval  17503  imasval  17560  imasvscaval  17587  homffval  17741  homfeq  17745  comfffval  17749  comffval  17750  comfffval2  17752  comffval2  17753  comfeq  17757  oppcval  17764  monfval  17784  sectffval  17802  invffval  17810  isofn  17827  cofuval  17934  natfval  18001  fucval  18013  fucco  18017  coafval  18116  setcval  18129  setcco  18135  catcval  18152  catcco  18157  estrcval  18175  estrcco  18181  xpcval  18228  1stfval  18242  2ndfval  18245  prfval  18250  evlfval  18268  evlf2  18269  curfval  18274  hofval  18303  hof2fval  18306  plusffval  18699  efmnd  18924  grpsubfval  19045  grpsubfvalALT  19046  grpsubpropd  19106  mulgfval  19130  mulgfvalALT  19131  mulgpropd  19177  lsmfval  19703  pj1fval  19759  efgtf  19787  prdsmgp  20222  dvrfval  20480  funcrngcsetcALT  20740  scaffval  21001  ipffval  21798  phssip  21808  frlmip  21928  psrval  22065  mamufval  22549  mvmulfval  22699  marrepfval  22717  marepvfval  22722  submafval  22736  submaval  22738  madufval  22794  minmar1fval  22803  mat2pmatfval  22880  cpm2mfval  22906  decpmatval0  22921  decpmatval  22922  pmatcollpw3lem  22940  xkoval  23744  xkopt  23812  xpstopnlem1  23966  submtmd  24261  blfvalps  24540  ishtpy  25131  isphtpy  25140  pcofval  25169  rrxip  25549  q1pval  26312  r1pval  26315  taylfval  26522  istrkgl  28727  tgplnfn  29057  plngval  29059  isplng  29060  midf  29085  ismidb  29087  ttgval  29224  wwlksnon  30200  wspthsnon  30201  clwwlknonmpo  30440  grpodivfval  30886  dipfval  31054  rlocval  33579  idlsrgval  33793  splyval  33949  submatres  34196  lmatval  34203  lmatcl  34206  qqhval  34362  sxval  34580  sitmval  34739  cndprobval  34823  mclsval  36055  csbfinxpg  38034  rrnval  38478  ldualset  39899  paddfval  40571  tgrpfset  41518  tgrpset  41519  erngfset  41573  erngset  41574  erngfset-rN  41581  erngset-rN  41582  dvafset  41778  dvaset  41779  dvhfset  41854  dvhset  41855  djaffvalN  41907  djafvalN  41908  djhffval  42170  djhfval  42171  hlhilset  42708  eldiophb  43488  mendval  43906  mnringvald  44937  mnringmulrd  44947  hoidmvval  47291  ovnhoi  47317  hspval  47323  hspmbllem2  47341  hoimbl  47345  rngcvalALTV  49030  rngccoALTV  49036  ringcvalALTV  49054  ringccoALTV  49070  lincop  49188  lines  49511  rrxlines  49513  spheres  49526  invfn  49808  infsubc2  49839  imaidfu2  49889  upfval  49954  dfswapf2  50039  swapfval  50040  1stfpropd  50068  2ndfpropd  50069  fucofvalg  50096  fuco21  50114  precofval3  50149  prcofvalg  50154  setc1ocofval  50272  lanfval  50391  ranfval  50392