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 2109   ∈ cmpo 7412

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-oprab 7414  df-mpo 7415

This theorem is referenced by:  mpoeq123i  7488  mptmpoopabbrd  8084  mptmpoopabbrdOLD  8085  mptmpoopabbrdOLDOLD  8087  el2mpocsbcl  8089  bropopvvv  8094  bropfvvvv  8096  prdsval  17474  imasval  17530  imasvscaval  17557  homffval  17707  homfeq  17711  comfffval  17715  comffval  17716  comfffval2  17718  comffval2  17719  comfeq  17723  oppcval  17730  monfval  17750  sectffval  17768  invffval  17776  isofn  17793  cofuval  17900  natfval  17967  fucval  17979  fucco  17983  coafval  18082  setcval  18095  setcco  18101  catcval  18118  catcco  18123  estrcval  18141  estrcco  18147  xpcval  18194  1stfval  18208  2ndfval  18211  prfval  18216  evlfval  18234  evlf2  18235  curfval  18240  hofval  18269  hof2fval  18272  plusffval  18629  efmnd  18853  grpsubfval  18971  grpsubfvalALT  18972  grpsubpropd  19033  mulgfval  19057  mulgfvalALT  19058  mulgpropd  19104  lsmfval  19624  pj1fval  19680  efgtf  19708  prdsmgp  20116  dvrfval  20367  funcrngcsetcALT  20606  scaffval  20842  ipffval  21613  phssip  21623  frlmip  21743  psrval  21880  mamufval  22335  mvmulfval  22485  marrepfval  22503  marepvfval  22508  submafval  22522  submaval  22524  madufval  22580  minmar1fval  22589  mat2pmatfval  22666  cpm2mfval  22692  decpmatval0  22707  decpmatval  22708  pmatcollpw3lem  22726  xkoval  23530  xkopt  23598  xpstopnlem1  23752  submtmd  24047  blfvalps  24327  ishtpy  24927  isphtpy  24936  pcofval  24966  rrxip  25347  q1pval  26117  r1pval  26120  taylfval  26323  istrkgl  28442  midf  28760  ismidb  28762  ttgval  28859  wwlksnon  29838  wspthsnon  29839  clwwlknonmpo  30075  grpodivfval  30520  dipfval  30688  rlocval  33259  idlsrgval  33523  submatres  33842  lmatval  33849  lmatcl  33852  qqhval  34008  sxval  34226  sitmval  34386  cndprobval  34470  mclsval  35590  csbfinxpg  37411  rrnval  37856  ldualset  39148  paddfval  39821  tgrpfset  40768  tgrpset  40769  erngfset  40823  erngset  40824  erngfset-rN  40831  erngset-rN  40832  dvafset  41028  dvaset  41029  dvhfset  41104  dvhset  41105  djaffvalN  41157  djafvalN  41158  djhffval  41420  djhfval  41421  hlhilset  41958  eldiophb  42755  mendval  43178  mnringvald  44212  mnringmulrd  44222  hoidmvval  46586  ovnhoi  46612  hspval  46618  hspmbllem2  46636  hoimbl  46640  rngcvalALTV  48220  rngccoALTV  48226  ringcvalALTV  48244  ringccoALTV  48260  lincop  48364  lines  48691  rrxlines  48693  spheres  48706  invfn  48980  infsubc2  49008  imaidfu2  49050  upfval  49091  dfswapf2  49158  swapfval  49159  fucofvalg  49209  fuco21  49227  precofval3  49262  prcofvalg  49267  setc1ocofval  49359  lanfval  49470  ranfval  49471