Theorem mpoeq123dv 7498

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

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

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-oprab 7427  df-mpo 7428

This theorem is used by:  mpoeq123i  7499  mptmpoopabbrd  8087  el2mpocsbcl  8089  bropopvvv  8094  bropfvvvv  8096  prdsval  17533  imasval  17590  imasvscaval  17617  homffval  17771  homfeq  17775  comfffval  17779  comffval  17780  comfffval2  17782  comffval2  17783  comfeq  17787  oppcval  17794  monfval  17814  sectffval  17832  invffval  17840  isofn  17857  cofuval  17964  natfval  18031  fucval  18043  fucco  18047  coafval  18146  setcval  18159  setcco  18165  catcval  18182  catcco  18187  estrcval  18205  estrcco  18211  xpcval  18258  1stfval  18272  2ndfval  18275  prfval  18280  evlfval  18298  evlf2  18299  curfval  18304  hofval  18333  hof2fval  18336  plusffval  18729  efmnd  18954  grpsubfval  19075  grpsubfvalALT  19076  grpsubpropd  19136  mulgfval  19160  mulgfvalALT  19161  mulgpropd  19207  lsmfval  19733  pj1fval  19789  efgtf  19817  prdsmgp  20252  dvrfval  20510  funcrngcsetcALT  20770  scaffval  21031  ipffval  21828  phssip  21838  frlmip  21958  psrval  22095  mamufval  22579  mvmulfval  22729  marrepfval  22747  marepvfval  22752  submafval  22766  submaval  22768  madufval  22824  minmar1fval  22833  mat2pmatfval  22910  cpm2mfval  22936  decpmatval0  22951  decpmatval  22952  pmatcollpw3lem  22970  xkoval  23774  xkopt  23842  xpstopnlem1  23996  submtmd  24291  blfvalps  24570  ishtpy  25161  isphtpy  25170  pcofval  25199  rrxip  25579  q1pval  26342  r1pval  26345  taylfval  26552  istrkgl  28757  tgplnfn  29087  plngval  29089  isplng  29090  midf  29115  ismidb  29117  ttgval  29254  wwlksnon  30230  wspthsnon  30231  clwwlknonmpo  30470  grpodivfval  30916  dipfval  31084  rlocval  33603  idlsrgval  33817  splyval  33973  submatres  34220  lmatval  34227  lmatcl  34230  qqhval  34386  sxval  34604  sitmval  34763  cndprobval  34847  mclsval  36068  csbfinxpg  38067  rrnval  38511  ldualset  39932  paddfval  40604  tgrpfset  41551  tgrpset  41552  erngfset  41606  erngset  41607  erngfset-rN  41614  erngset-rN  41615  dvafset  41811  dvaset  41812  dvhfset  41887  dvhset  41888  djaffvalN  41940  djafvalN  41941  djhffval  42203  djhfval  42204  hlhilset  42741  eldiophb  43521  mendval  43939  mnringvald  44970  mnringmulrd  44980  hoidmvval  47324  ovnhoi  47350  hspval  47356  hspmbllem2  47374  hoimbl  47378  rngcvalALTV  49063  rngccoALTV  49069  ringcvalALTV  49087  ringccoALTV  49103  lincop  49221  lines  49544  rrxlines  49546  spheres  49559  invfn  49841  infsubc2  49872  imaidfu2  49922  upfval  49987  dfswapf2  50072  swapfval  50073  1stfpropd  50101  2ndfpropd  50102  fucofvalg  50129  fuco21  50147  precofval3  50182  prcofvalg  50187  setc1ocofval  50305  lanfval  50424  ranfval  50425