Theorem mpoeq123dv 7526

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-oprab 7455  df-mpo 7456

This theorem is used by:  mpoeq123i  7527  mptmpoopabbrd  8129  el2mpocsbcl  8131  bropopvvv  8136  bropfvvvv  8138  prdsval  17676  imasval  17733  imasvscaval  17760  homffval  17914  homfeq  17918  comfffval  17922  comffval  17923  comfffval2  17925  comffval2  17926  comfeq  17930  oppcval  17937  monfval  17957  sectffval  17975  invffval  17983  isofn  18000  cofuval  18107  natfval  18174  fucval  18186  fucco  18190  coafval  18289  setcval  18302  setcco  18308  catcval  18325  catcco  18330  estrcval  18348  estrcco  18354  xpcval  18401  1stfval  18415  2ndfval  18418  prfval  18423  evlfval  18441  evlf2  18442  curfval  18447  hofval  18476  hof2fval  18479  plusffval  18872  efmnd  19116  grpsubfval  19244  grpsubfvalALT  19245  grpsubpropd  19305  mulgfval  19329  mulgfvalALT  19330  mulgpropd  19376  lsmfval  19903  pj1fval  19959  efgtf  19987  prdsmgp  20422  dvrfval  20683  funcrngcsetcALT  20944  scaffval  21206  ipffval  22009  phssip  22019  frlmip  22139  psrval  22278  mamufval  22762  mvmulfval  22912  marrepfval  22930  marepvfval  22935  submafval  22949  submaval  22951  madufval  23007  minmar1fval  23016  mat2pmatfval  23096  cpm2mfval  23122  decpmatval0  23137  decpmatval  23138  pmatcollpw3lem  23156  xkoval  23961  xkopt  24029  xpstopnlem1  24183  submtmd  24478  blfvalps  24757  ishtpy  25348  isphtpy  25357  pcofval  25386  rrxip  25766  q1pval  26528  r1pval  26531  taylfval  26743  istrkgl  28977  tgplnfn  29310  plngval  29312  isplng  29313  midf  29338  ismidb  29340  angmgmval  29451  ttgval  29509  wwlksnon  30497  wspthsnon  30498  clwwlknonmpo  30737  grpodivfval  31193  dipfval  31361  rlocval  33919  idlsrgval  34139  splyval  34302  submatres  34549  lmatval  34556  lmatcl  34559  qqhval  34715  sxval  34934  sitmval  35092  cndprobval  35176  mclsval  36536  csbfinxpg  38579  rrnval  39027  ldualset  40448  paddfval  41120  tgrpfset  42067  tgrpset  42068  erngfset  42122  erngset  42123  erngfset-rN  42130  erngset-rN  42131  dvafset  42327  dvaset  42328  dvhfset  42403  dvhset  42404  djaffvalN  42456  djafvalN  42457  djhffval  42719  djhfval  42720  hlhilset  43257  eldiophb  44034  mendval  44442  mnringvald  45472  mnringmulrd  45482  hoidmvval  47860  ovnhoi  47886  hspval  47892  hspmbllem2  47910  hoimbl  47914  rngcvalALTV  49635  rngccoALTV  49641  ringcvalALTV  49659  ringccoALTV  49675  lincop  49851  lines  50175  rrxlines  50177  spheres  50189  invfn  50475  infsubc2  50506  imaidfu2  50558  upfval  50623  dfswapf2  50714  swapfval  50715  1stfpropd  50743  2ndfpropd  50744  fucofvalg  50771  fuco21  50789  precofval3  50837  prcofvalg  50842  setc1ocofval  50960  lanfval  51127  ranfval  51128