Theorem mpoeq123dv 7359

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107   ∈ cmpo 7286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-oprab 7288  df-mpo 7289

This theorem is referenced by:  mpoeq123i  7360  mptmpoopabbrd  7930  mptmpoopabbrdOLD  7932  el2mpocsbcl  7934  bropopvvv  7939  bropfvvvv  7941  prdsval  17175  imasval  17231  imasvscaval  17258  homffval  17408  homfeq  17412  comfffval  17416  comffval  17417  comfffval2  17419  comffval2  17420  comfeq  17424  oppcval  17431  monfval  17453  sectffval  17471  invffval  17479  isofn  17496  cofuval  17606  natfval  17671  fucval  17684  fucco  17689  coafval  17788  setcval  17801  setcco  17807  catcval  17824  catcco  17829  estrcval  17849  estrcco  17855  xpcval  17903  1stfval  17917  2ndfval  17920  prfval  17925  evlfval  17944  evlf2  17945  curfval  17950  hofval  17979  hof2fval  17982  plusffval  18341  efmnd  18518  grpsubfval  18632  grpsubfvalALT  18633  grpsubpropd  18689  mulgfval  18711  mulgfvalALT  18712  mulgpropd  18754  lsmfval  19252  pj1fval  19309  efgtf  19337  prdsmgp  19858  dvrfval  19935  scaffval  20150  ipffval  20862  phssip  20872  frlmip  20994  psrval  21127  mamufval  21543  mvmulfval  21700  marrepfval  21718  marepvfval  21723  submafval  21737  submaval  21739  madufval  21795  minmar1fval  21804  mat2pmatfval  21881  cpm2mfval  21907  decpmatval0  21922  decpmatval  21923  pmatcollpw3lem  21941  xkoval  22747  xkopt  22815  xpstopnlem1  22969  submtmd  23264  blfvalps  23545  ishtpy  24144  isphtpy  24153  pcofval  24182  rrxip  24563  q1pval  25327  r1pval  25330  taylfval  25527  midf  27146  ismidb  27148  ttgval  27245  ttgvalOLD  27246  wwlksnon  28225  wspthsnon  28226  clwwlknonmpo  28462  grpodivfval  28905  dipfval  29073  idlsrgval  31657  submatres  31765  lmatval  31772  lmatcl  31775  qqhval  31933  sxval  32167  sitmval  32325  cndprobval  32409  mclsval  33534  csbfinxpg  35568  rrnval  35994  ldualset  37146  paddfval  37818  tgrpfset  38765  tgrpset  38766  erngfset  38820  erngset  38821  erngfset-rN  38828  erngset-rN  38829  dvafset  39025  dvaset  39026  dvhfset  39101  dvhset  39102  djaffvalN  39154  djafvalN  39155  djhffval  39417  djhfval  39418  hlhilset  39955  eldiophb  40586  mendval  41015  mnringvald  41833  mnringmulrd  41846  hoidmvval  44122  ovnhoi  44148  hspval  44154  hspmbllem2  44172  hoimbl  44176  rngcvalALTV  45530  rngccoALTV  45557  funcrngcsetcALT  45568  ringcvalALTV  45576  ringccoALTV  45620  lincop  45760  lines  46088  rrxlines  46090  spheres  46103