Theorem mpoeq123dv 7500

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534   ∈ wcel 2099   ∈ cmpo 7426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-oprab 7428  df-mpo 7429

This theorem is referenced by:  mpoeq123i  7501  mptmpoopabbrd  8094  mptmpoopabbrdOLD  8095  mptmpoopabbrdOLDOLD  8097  el2mpocsbcl  8099  bropopvvv  8104  bropfvvvv  8106  prdsval  17470  imasval  17526  imasvscaval  17553  homffval  17703  homfeq  17707  comfffval  17711  comffval  17712  comfffval2  17714  comffval2  17715  comfeq  17719  oppcval  17726  monfval  17748  sectffval  17766  invffval  17774  isofn  17791  cofuval  17901  natfval  17969  fucval  17982  fucco  17987  coafval  18086  setcval  18099  setcco  18105  catcval  18122  catcco  18127  estrcval  18147  estrcco  18153  xpcval  18201  1stfval  18215  2ndfval  18218  prfval  18223  evlfval  18242  evlf2  18243  curfval  18248  hofval  18277  hof2fval  18280  plusffval  18639  efmnd  18860  grpsubfval  18978  grpsubfvalALT  18979  grpsubpropd  19039  mulgfval  19063  mulgfvalALT  19064  mulgpropd  19110  lsmfval  19636  pj1fval  19692  efgtf  19720  prdsmgp  20134  dvrfval  20384  funcrngcsetcALT  20619  scaffval  20856  ipffval  21644  phssip  21654  frlmip  21776  psrval  21912  mamufval  22383  mvmulfval  22535  marrepfval  22553  marepvfval  22558  submafval  22572  submaval  22574  madufval  22630  minmar1fval  22639  mat2pmatfval  22716  cpm2mfval  22742  decpmatval0  22757  decpmatval  22758  pmatcollpw3lem  22776  xkoval  23582  xkopt  23650  xpstopnlem1  23804  submtmd  24099  blfvalps  24380  ishtpy  24989  isphtpy  24998  pcofval  25028  rrxip  25409  q1pval  26182  r1pval  26185  taylfval  26386  istrkgl  28385  midf  28703  ismidb  28705  ttgval  28802  ttgvalOLD  28803  wwlksnon  29785  wspthsnon  29786  clwwlknonmpo  30022  grpodivfval  30467  dipfval  30635  rlocval  33114  idlsrgval  33378  submatres  33621  lmatval  33628  lmatcl  33631  qqhval  33789  sxval  34023  sitmval  34183  cndprobval  34267  mclsval  35391  csbfinxpg  37095  rrnval  37528  ldualset  38823  paddfval  39496  tgrpfset  40443  tgrpset  40444  erngfset  40498  erngset  40499  erngfset-rN  40506  erngset-rN  40507  dvafset  40703  dvaset  40704  dvhfset  40779  dvhset  40780  djaffvalN  40832  djafvalN  40833  djhffval  41095  djhfval  41096  hlhilset  41633  eldiophb  42414  mendval  42844  mnringvald  43882  mnringmulrd  43895  hoidmvval  46198  ovnhoi  46224  hspval  46230  hspmbllem2  46248  hoimbl  46252  rngcvalALTV  47642  rngccoALTV  47648  ringcvalALTV  47666  ringccoALTV  47682  lincop  47791  lines  48119  rrxlines  48121  spheres  48134