Theorem mpoeq123dv 7442

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-oprab 7371  df-mpo 7372

This theorem is referenced by:  mpoeq123i  7443  mptmpoopabbrd  8033  el2mpocsbcl  8035  bropopvvv  8040  bropfvvvv  8042  prdsval  17418  imasval  17475  imasvscaval  17502  homffval  17656  homfeq  17660  comfffval  17664  comffval  17665  comfffval2  17667  comffval2  17668  comfeq  17672  oppcval  17679  monfval  17699  sectffval  17717  invffval  17725  isofn  17742  cofuval  17849  natfval  17916  fucval  17928  fucco  17932  coafval  18031  setcval  18044  setcco  18050  catcval  18067  catcco  18072  estrcval  18090  estrcco  18096  xpcval  18143  1stfval  18157  2ndfval  18160  prfval  18165  evlfval  18183  evlf2  18184  curfval  18189  hofval  18218  hof2fval  18221  plusffval  18614  efmnd  18838  grpsubfval  18959  grpsubfvalALT  18960  grpsubpropd  19021  mulgfval  19045  mulgfvalALT  19046  mulgpropd  19092  lsmfval  19613  pj1fval  19669  efgtf  19697  prdsmgp  20132  dvrfval  20382  funcrngcsetcALT  20618  scaffval  20875  ipffval  21628  phssip  21638  frlmip  21758  psrval  21895  mamufval  22357  mvmulfval  22507  marrepfval  22525  marepvfval  22530  submafval  22544  submaval  22546  madufval  22602  minmar1fval  22611  mat2pmatfval  22688  cpm2mfval  22714  decpmatval0  22729  decpmatval  22730  pmatcollpw3lem  22748  xkoval  23552  xkopt  23620  xpstopnlem1  23774  submtmd  24069  blfvalps  24348  ishtpy  24939  isphtpy  24948  pcofval  24977  rrxip  25357  q1pval  26120  r1pval  26123  taylfval  26324  istrkgl  28526  midf  28844  ismidb  28846  ttgval  28943  wwlksnon  29919  wspthsnon  29920  clwwlknonmpo  30159  grpodivfval  30605  dipfval  30773  rlocval  33320  idlsrgval  33563  splyval  33703  submatres  33950  lmatval  33957  lmatcl  33960  qqhval  34116  sxval  34334  sitmval  34493  cndprobval  34577  mclsval  35745  csbfinxpg  37704  rrnval  38148  ldualset  39571  paddfval  40243  tgrpfset  41190  tgrpset  41191  erngfset  41245  erngset  41246  erngfset-rN  41253  erngset-rN  41254  dvafset  41450  dvaset  41451  dvhfset  41526  dvhset  41527  djaffvalN  41579  djafvalN  41580  djhffval  41842  djhfval  41843  hlhilset  42380  eldiophb  43189  mendval  43607  mnringvald  44640  mnringmulrd  44650  hoidmvval  47005  ovnhoi  47031  hspval  47037  hspmbllem2  47055  hoimbl  47059  rngcvalALTV  48741  rngccoALTV  48747  ringcvalALTV  48765  ringccoALTV  48781  lincop  48884  lines  49207  rrxlines  49209  spheres  49222  invfn  49505  infsubc2  49536  imaidfu2  49586  upfval  49651  dfswapf2  49736  swapfval  49737  1stfpropd  49765  2ndfpropd  49766  fucofvalg  49793  fuco21  49811  precofval3  49846  prcofvalg  49851  setc1ocofval  49969  lanfval  50088  ranfval  50089