Theorem mpoeq123dv 7493

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-oprab 7422  df-mpo 7423

This theorem is used by:  mpoeq123i  7494  mptmpoopabbrd  8092  el2mpocsbcl  8094  bropopvvv  8099  bropfvvvv  8101  prdsval  17619  imasval  17676  imasvscaval  17703  homffval  17857  homfeq  17861  comfffval  17865  comffval  17866  comfffval2  17868  comffval2  17869  comfeq  17873  oppcval  17880  monfval  17900  sectffval  17918  invffval  17926  isofn  17943  cofuval  18050  natfval  18117  fucval  18129  fucco  18133  coafval  18232  setcval  18245  setcco  18251  catcval  18268  catcco  18273  estrcval  18291  estrcco  18297  xpcval  18344  1stfval  18358  2ndfval  18361  prfval  18366  evlfval  18384  evlf2  18385  curfval  18390  hofval  18419  hof2fval  18422  plusffval  18815  efmnd  19059  grpsubfval  19187  grpsubfvalALT  19188  grpsubpropd  19248  mulgfval  19272  mulgfvalALT  19273  mulgpropd  19319  lsmfval  19845  pj1fval  19901  efgtf  19929  prdsmgp  20364  dvrfval  20625  funcrngcsetcALT  20886  scaffval  21148  ipffval  21947  phssip  21957  frlmip  22077  psrval  22216  mamufval  22700  mvmulfval  22850  marrepfval  22868  marepvfval  22873  submafval  22887  submaval  22889  madufval  22945  minmar1fval  22954  mat2pmatfval  23034  cpm2mfval  23060  decpmatval0  23075  decpmatval  23076  pmatcollpw3lem  23094  xkoval  23899  xkopt  23967  xpstopnlem1  24121  submtmd  24416  blfvalps  24695  ishtpy  25286  isphtpy  25295  pcofval  25324  rrxip  25704  q1pval  26466  r1pval  26469  taylfval  26679  istrkgl  28913  tgplnfn  29246  plngval  29248  isplng  29249  midf  29274  ismidb  29276  angmgmval  29387  ttgval  29445  wwlksnon  30433  wspthsnon  30434  clwwlknonmpo  30673  grpodivfval  31129  dipfval  31297  rlocval  33813  idlsrgval  34028  splyval  34184  submatres  34431  lmatval  34438  lmatcl  34441  qqhval  34597  sxval  34816  sitmval  34974  cndprobval  35058  mclsval  36307  csbfinxpg  38291  rrnval  38741  ldualset  40162  paddfval  40834  tgrpfset  41781  tgrpset  41782  erngfset  41836  erngset  41837  erngfset-rN  41844  erngset-rN  41845  dvafset  42041  dvaset  42042  dvhfset  42117  dvhset  42118  djaffvalN  42170  djafvalN  42171  djhffval  42433  djhfval  42434  hlhilset  42971  eldiophb  43747  mendval  44165  mnringvald  45196  mnringmulrd  45206  hoidmvval  47556  ovnhoi  47582  hspval  47588  hspmbllem2  47606  hoimbl  47610  rngcvalALTV  49331  rngccoALTV  49337  ringcvalALTV  49355  ringccoALTV  49371  lincop  49489  lines  49812  rrxlines  49814  spheres  49827  invfn  50107  infsubc2  50138  imaidfu2  50188  upfval  50253  dfswapf2  50338  swapfval  50339  1stfpropd  50367  2ndfpropd  50368  fucofvalg  50395  fuco21  50413  precofval3  50448  prcofvalg  50453  setc1ocofval  50571  lanfval  50690  ranfval  50691