Theorem mpoeq123dv 7435

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ∈ cmpo 7362

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-oprab 7364  df-mpo 7365

This theorem is referenced by:  mpoeq123i  7436  mptmpoopabbrd  8026  el2mpocsbcl  8028  bropopvvv  8033  bropfvvvv  8035  prdsval  17409  imasval  17466  imasvscaval  17493  homffval  17647  homfeq  17651  comfffval  17655  comffval  17656  comfffval2  17658  comffval2  17659  comfeq  17663  oppcval  17670  monfval  17690  sectffval  17708  invffval  17716  isofn  17733  cofuval  17840  natfval  17907  fucval  17919  fucco  17923  coafval  18022  setcval  18035  setcco  18041  catcval  18058  catcco  18063  estrcval  18081  estrcco  18087  xpcval  18134  1stfval  18148  2ndfval  18151  prfval  18156  evlfval  18174  evlf2  18175  curfval  18180  hofval  18209  hof2fval  18212  plusffval  18605  efmnd  18829  grpsubfval  18950  grpsubfvalALT  18951  grpsubpropd  19012  mulgfval  19036  mulgfvalALT  19037  mulgpropd  19083  lsmfval  19604  pj1fval  19660  efgtf  19688  prdsmgp  20123  dvrfval  20373  funcrngcsetcALT  20609  scaffval  20866  ipffval  21638  phssip  21648  frlmip  21768  psrval  21905  mamufval  22367  mvmulfval  22517  marrepfval  22535  marepvfval  22540  submafval  22554  submaval  22556  madufval  22612  minmar1fval  22621  mat2pmatfval  22698  cpm2mfval  22724  decpmatval0  22739  decpmatval  22740  pmatcollpw3lem  22758  xkoval  23562  xkopt  23630  xpstopnlem1  23784  submtmd  24079  blfvalps  24358  ishtpy  24949  isphtpy  24958  pcofval  24987  rrxip  25367  q1pval  26130  r1pval  26133  taylfval  26335  istrkgl  28540  midf  28858  ismidb  28860  ttgval  28957  wwlksnon  29934  wspthsnon  29935  clwwlknonmpo  30174  grpodivfval  30620  dipfval  30788  rlocval  33335  idlsrgval  33578  splyval  33718  submatres  33966  lmatval  33973  lmatcl  33976  qqhval  34132  sxval  34350  sitmval  34509  cndprobval  34593  mclsval  35761  csbfinxpg  37718  rrnval  38162  ldualset  39585  paddfval  40257  tgrpfset  41204  tgrpset  41205  erngfset  41259  erngset  41260  erngfset-rN  41267  erngset-rN  41268  dvafset  41464  dvaset  41465  dvhfset  41540  dvhset  41541  djaffvalN  41593  djafvalN  41594  djhffval  41856  djhfval  41857  hlhilset  42394  eldiophb  43203  mendval  43625  mnringvald  44658  mnringmulrd  44668  hoidmvval  47023  ovnhoi  47049  hspval  47055  hspmbllem2  47073  hoimbl  47077  rngcvalALTV  48753  rngccoALTV  48759  ringcvalALTV  48777  ringccoALTV  48793  lincop  48896  lines  49219  rrxlines  49221  spheres  49234  invfn  49517  infsubc2  49548  imaidfu2  49598  upfval  49663  dfswapf2  49748  swapfval  49749  1stfpropd  49777  2ndfpropd  49778  fucofvalg  49805  fuco21  49823  precofval3  49858  prcofvalg  49863  setc1ocofval  49981  lanfval  50100  ranfval  50101