Theorem mpoeq123dv 7488

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ∈ cmpo 7415

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-oprab 7417  df-mpo 7418

This theorem is used by:  mpoeq123i  7489  mptmpoopabbrd  8080  el2mpocsbcl  8082  bropopvvv  8087  bropfvvvv  8089  prdsval  17540  imasval  17597  imasvscaval  17624  homffval  17778  homfeq  17782  comfffval  17786  comffval  17787  comfffval2  17789  comffval2  17790  comfeq  17794  oppcval  17801  monfval  17821  sectffval  17839  invffval  17847  isofn  17864  cofuval  17971  natfval  18038  fucval  18050  fucco  18054  coafval  18153  setcval  18166  setcco  18172  catcval  18189  catcco  18194  estrcval  18212  estrcco  18218  xpcval  18265  1stfval  18279  2ndfval  18282  prfval  18287  evlfval  18305  evlf2  18306  curfval  18311  hofval  18340  hof2fval  18343  plusffval  18736  efmnd  18979  grpsubfval  19107  grpsubfvalALT  19108  grpsubpropd  19168  mulgfval  19192  mulgfvalALT  19193  mulgpropd  19239  lsmfval  19765  pj1fval  19821  efgtf  19849  prdsmgp  20284  dvrfval  20543  funcrngcsetcALT  20803  scaffval  21064  ipffval  21861  phssip  21871  frlmip  21991  psrval  22130  mamufval  22614  mvmulfval  22764  marrepfval  22782  marepvfval  22787  submafval  22801  submaval  22803  madufval  22859  minmar1fval  22868  mat2pmatfval  22948  cpm2mfval  22974  decpmatval0  22989  decpmatval  22990  pmatcollpw3lem  23008  xkoval  23813  xkopt  23881  xpstopnlem1  24035  submtmd  24330  blfvalps  24609  ishtpy  25200  isphtpy  25209  pcofval  25238  rrxip  25618  q1pval  26380  r1pval  26383  taylfval  26595  istrkgl  28799  tgplnfn  29132  plngval  29134  isplng  29135  midf  29160  ismidb  29162  angmgmval  29273  ttgval  29331  wwlksnon  30319  wspthsnon  30320  clwwlknonmpo  30559  grpodivfval  31015  dipfval  31183  rlocval  33699  idlsrgval  33913  splyval  34069  submatres  34316  lmatval  34323  lmatcl  34326  qqhval  34482  sxval  34701  sitmval  34860  cndprobval  34944  mclsval  36142  csbfinxpg  38142  rrnval  38577  ldualset  39998  paddfval  40670  tgrpfset  41617  tgrpset  41618  erngfset  41672  erngset  41673  erngfset-rN  41680  erngset-rN  41681  dvafset  41877  dvaset  41878  dvhfset  41953  dvhset  41954  djaffvalN  42006  djafvalN  42007  djhffval  42269  djhfval  42270  hlhilset  42807  eldiophb  43602  mendval  44020  mnringvald  45051  mnringmulrd  45061  hoidmvval  47405  ovnhoi  47431  hspval  47437  hspmbllem2  47455  hoimbl  47459  rngcvalALTV  49180  rngccoALTV  49186  ringcvalALTV  49204  ringccoALTV  49220  lincop  49338  lines  49661  rrxlines  49663  spheres  49676  invfn  49956  infsubc2  49987  imaidfu2  50037  upfval  50102  dfswapf2  50187  swapfval  50188  1stfpropd  50216  2ndfpropd  50217  fucofvalg  50244  fuco21  50262  precofval3  50297  prcofvalg  50302  setc1ocofval  50420  lanfval  50539  ranfval  50540