Theorem mpoeq123dv 7424

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ∈ cmpo 7351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-oprab 7353  df-mpo 7354

This theorem is referenced by:  mpoeq123i  7425  mptmpoopabbrd  8015  mptmpoopabbrdOLD  8016  el2mpocsbcl  8018  bropopvvv  8023  bropfvvvv  8025  prdsval  17359  imasval  17415  imasvscaval  17442  homffval  17596  homfeq  17600  comfffval  17604  comffval  17605  comfffval2  17607  comffval2  17608  comfeq  17612  oppcval  17619  monfval  17639  sectffval  17657  invffval  17665  isofn  17682  cofuval  17789  natfval  17856  fucval  17868  fucco  17872  coafval  17971  setcval  17984  setcco  17990  catcval  18007  catcco  18012  estrcval  18030  estrcco  18036  xpcval  18083  1stfval  18097  2ndfval  18100  prfval  18105  evlfval  18123  evlf2  18124  curfval  18129  hofval  18158  hof2fval  18161  plusffval  18520  efmnd  18744  grpsubfval  18862  grpsubfvalALT  18863  grpsubpropd  18924  mulgfval  18948  mulgfvalALT  18949  mulgpropd  18995  lsmfval  19517  pj1fval  19573  efgtf  19601  prdsmgp  20036  dvrfval  20287  funcrngcsetcALT  20526  scaffval  20783  ipffval  21555  phssip  21565  frlmip  21685  psrval  21822  mamufval  22277  mvmulfval  22427  marrepfval  22445  marepvfval  22450  submafval  22464  submaval  22466  madufval  22522  minmar1fval  22531  mat2pmatfval  22608  cpm2mfval  22634  decpmatval0  22649  decpmatval  22650  pmatcollpw3lem  22668  xkoval  23472  xkopt  23540  xpstopnlem1  23694  submtmd  23989  blfvalps  24269  ishtpy  24869  isphtpy  24878  pcofval  24908  rrxip  25288  q1pval  26058  r1pval  26061  taylfval  26264  istrkgl  28403  midf  28721  ismidb  28723  ttgval  28820  wwlksnon  29796  wspthsnon  29797  clwwlknonmpo  30033  grpodivfval  30478  dipfval  30646  rlocval  33199  idlsrgval  33440  submatres  33773  lmatval  33780  lmatcl  33783  qqhval  33939  sxval  34157  sitmval  34317  cndprobval  34401  mclsval  35536  csbfinxpg  37362  rrnval  37807  ldualset  39104  paddfval  39776  tgrpfset  40723  tgrpset  40724  erngfset  40778  erngset  40779  erngfset-rN  40786  erngset-rN  40787  dvafset  40983  dvaset  40984  dvhfset  41059  dvhset  41060  djaffvalN  41112  djafvalN  41113  djhffval  41375  djhfval  41376  hlhilset  41913  eldiophb  42730  mendval  43152  mnringvald  44186  mnringmulrd  44196  hoidmvval  46558  ovnhoi  46584  hspval  46590  hspmbllem2  46608  hoimbl  46612  rngcvalALTV  48249  rngccoALTV  48255  ringcvalALTV  48273  ringccoALTV  48289  lincop  48393  lines  48716  rrxlines  48718  spheres  48731  invfn  49015  infsubc2  49046  imaidfu2  49096  upfval  49161  dfswapf2  49246  swapfval  49247  1stfpropd  49275  2ndfpropd  49276  fucofvalg  49303  fuco21  49321  precofval3  49356  prcofvalg  49361  setc1ocofval  49479  lanfval  49598  ranfval  49599