Theorem mpoeq123dv 7433

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ∈ cmpo 7360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-oprab 7362  df-mpo 7363

This theorem is referenced by:  mpoeq123i  7434  mptmpoopabbrd  8024  mptmpoopabbrdOLD  8025  el2mpocsbcl  8027  bropopvvv  8032  bropfvvvv  8034  prdsval  17375  imasval  17432  imasvscaval  17459  homffval  17613  homfeq  17617  comfffval  17621  comffval  17622  comfffval2  17624  comffval2  17625  comfeq  17629  oppcval  17636  monfval  17656  sectffval  17674  invffval  17682  isofn  17699  cofuval  17806  natfval  17873  fucval  17885  fucco  17889  coafval  17988  setcval  18001  setcco  18007  catcval  18024  catcco  18029  estrcval  18047  estrcco  18053  xpcval  18100  1stfval  18114  2ndfval  18117  prfval  18122  evlfval  18140  evlf2  18141  curfval  18146  hofval  18175  hof2fval  18178  plusffval  18571  efmnd  18795  grpsubfval  18913  grpsubfvalALT  18914  grpsubpropd  18975  mulgfval  18999  mulgfvalALT  19000  mulgpropd  19046  lsmfval  19567  pj1fval  19623  efgtf  19651  prdsmgp  20086  dvrfval  20338  funcrngcsetcALT  20574  scaffval  20831  ipffval  21603  phssip  21613  frlmip  21733  psrval  21871  mamufval  22336  mvmulfval  22486  marrepfval  22504  marepvfval  22509  submafval  22523  submaval  22525  madufval  22581  minmar1fval  22590  mat2pmatfval  22667  cpm2mfval  22693  decpmatval0  22708  decpmatval  22709  pmatcollpw3lem  22727  xkoval  23531  xkopt  23599  xpstopnlem1  23753  submtmd  24048  blfvalps  24327  ishtpy  24927  isphtpy  24936  pcofval  24966  rrxip  25346  q1pval  26116  r1pval  26119  taylfval  26322  istrkgl  28530  midf  28848  ismidb  28850  ttgval  28947  wwlksnon  29924  wspthsnon  29925  clwwlknonmpo  30164  grpodivfval  30609  dipfval  30777  rlocval  33341  idlsrgval  33584  splyval  33717  submatres  33963  lmatval  33970  lmatcl  33973  qqhval  34129  sxval  34347  sitmval  34506  cndprobval  34590  mclsval  35757  csbfinxpg  37593  rrnval  38028  ldualset  39385  paddfval  40057  tgrpfset  41004  tgrpset  41005  erngfset  41059  erngset  41060  erngfset-rN  41067  erngset-rN  41068  dvafset  41264  dvaset  41265  dvhfset  41340  dvhset  41341  djaffvalN  41393  djafvalN  41394  djhffval  41656  djhfval  41657  hlhilset  42194  eldiophb  42999  mendval  43421  mnringvald  44454  mnringmulrd  44464  hoidmvval  46821  ovnhoi  46847  hspval  46853  hspmbllem2  46871  hoimbl  46875  rngcvalALTV  48511  rngccoALTV  48517  ringcvalALTV  48535  ringccoALTV  48551  lincop  48654  lines  48977  rrxlines  48979  spheres  48992  invfn  49275  infsubc2  49306  imaidfu2  49356  upfval  49421  dfswapf2  49506  swapfval  49507  1stfpropd  49535  2ndfpropd  49536  fucofvalg  49563  fuco21  49581  precofval3  49616  prcofvalg  49621  setc1ocofval  49739  lanfval  49858  ranfval  49859