Theorem mpoeq123dv 7424

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1541   ∈ wcel 2106   ∈ cmpo 7351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-oprab 7353  df-mpo 7354

This theorem is referenced by:  mpoeq123i  7425  mptmpoopabbrd  8001  mptmpoopabbrdOLD  8003  el2mpocsbcl  8005  bropopvvv  8010  bropfvvvv  8012  prdsval  17271  imasval  17327  imasvscaval  17354  homffval  17504  homfeq  17508  comfffval  17512  comffval  17513  comfffval2  17515  comffval2  17516  comfeq  17520  oppcval  17527  monfval  17549  sectffval  17567  invffval  17575  isofn  17592  cofuval  17702  natfval  17767  fucval  17780  fucco  17785  coafval  17884  setcval  17897  setcco  17903  catcval  17920  catcco  17925  estrcval  17945  estrcco  17951  xpcval  17999  1stfval  18013  2ndfval  18016  prfval  18021  evlfval  18040  evlf2  18041  curfval  18046  hofval  18075  hof2fval  18078  plusffval  18437  efmnd  18613  grpsubfval  18727  grpsubfvalALT  18728  grpsubpropd  18784  mulgfval  18806  mulgfvalALT  18807  mulgpropd  18849  lsmfval  19347  pj1fval  19403  efgtf  19431  prdsmgp  19951  dvrfval  20028  scaffval  20254  ipffval  20966  phssip  20976  frlmip  21098  psrval  21231  mamufval  21647  mvmulfval  21804  marrepfval  21822  marepvfval  21827  submafval  21841  submaval  21843  madufval  21899  minmar1fval  21908  mat2pmatfval  21985  cpm2mfval  22011  decpmatval0  22026  decpmatval  22027  pmatcollpw3lem  22045  xkoval  22851  xkopt  22919  xpstopnlem1  23073  submtmd  23368  blfvalps  23649  ishtpy  24248  isphtpy  24257  pcofval  24286  rrxip  24667  q1pval  25431  r1pval  25434  taylfval  25631  midf  27495  ismidb  27497  ttgval  27594  ttgvalOLD  27595  wwlksnon  28573  wspthsnon  28574  clwwlknonmpo  28810  grpodivfval  29253  dipfval  29421  idlsrgval  32012  submatres  32121  lmatval  32128  lmatcl  32131  qqhval  32289  sxval  32523  sitmval  32683  cndprobval  32767  mclsval  33891  csbfinxpg  35718  rrnval  36145  ldualset  37447  paddfval  38120  tgrpfset  39067  tgrpset  39068  erngfset  39122  erngset  39123  erngfset-rN  39130  erngset-rN  39131  dvafset  39327  dvaset  39328  dvhfset  39403  dvhset  39404  djaffvalN  39456  djafvalN  39457  djhffval  39719  djhfval  39720  hlhilset  40257  eldiophb  40896  mendval  41326  mnringvald  42203  mnringmulrd  42216  hoidmvval  44508  ovnhoi  44534  hspval  44540  hspmbllem2  44558  hoimbl  44562  rngcvalALTV  45941  rngccoALTV  45968  funcrngcsetcALT  45979  ringcvalALTV  45987  ringccoALTV  46031  lincop  46171  lines  46499  rrxlines  46501  spheres  46514