Theorem mpoeq123dv 7416

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111   ∈ cmpo 7343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-oprab 7345  df-mpo 7346

This theorem is referenced by:  mpoeq123i  7417  mptmpoopabbrd  8007  mptmpoopabbrdOLD  8008  el2mpocsbcl  8010  bropopvvv  8015  bropfvvvv  8017  prdsval  17354  imasval  17410  imasvscaval  17437  homffval  17591  homfeq  17595  comfffval  17599  comffval  17600  comfffval2  17602  comffval2  17603  comfeq  17607  oppcval  17614  monfval  17634  sectffval  17652  invffval  17660  isofn  17677  cofuval  17784  natfval  17851  fucval  17863  fucco  17867  coafval  17966  setcval  17979  setcco  17985  catcval  18002  catcco  18007  estrcval  18025  estrcco  18031  xpcval  18078  1stfval  18092  2ndfval  18095  prfval  18100  evlfval  18118  evlf2  18119  curfval  18124  hofval  18153  hof2fval  18156  plusffval  18549  efmnd  18773  grpsubfval  18891  grpsubfvalALT  18892  grpsubpropd  18953  mulgfval  18977  mulgfvalALT  18978  mulgpropd  19024  lsmfval  19545  pj1fval  19601  efgtf  19629  prdsmgp  20064  dvrfval  20315  funcrngcsetcALT  20551  scaffval  20808  ipffval  21580  phssip  21590  frlmip  21710  psrval  21847  mamufval  22302  mvmulfval  22452  marrepfval  22470  marepvfval  22475  submafval  22489  submaval  22491  madufval  22547  minmar1fval  22556  mat2pmatfval  22633  cpm2mfval  22659  decpmatval0  22674  decpmatval  22675  pmatcollpw3lem  22693  xkoval  23497  xkopt  23565  xpstopnlem1  23719  submtmd  24014  blfvalps  24293  ishtpy  24893  isphtpy  24902  pcofval  24932  rrxip  25312  q1pval  26082  r1pval  26085  taylfval  26288  istrkgl  28431  midf  28749  ismidb  28751  ttgval  28848  wwlksnon  29824  wspthsnon  29825  clwwlknonmpo  30061  grpodivfval  30506  dipfval  30674  rlocval  33218  idlsrgval  33460  splyval  33574  submatres  33811  lmatval  33818  lmatcl  33821  qqhval  33977  sxval  34195  sitmval  34354  cndprobval  34438  mclsval  35599  csbfinxpg  37422  rrnval  37867  ldualset  39164  paddfval  39836  tgrpfset  40783  tgrpset  40784  erngfset  40838  erngset  40839  erngfset-rN  40846  erngset-rN  40847  dvafset  41043  dvaset  41044  dvhfset  41119  dvhset  41120  djaffvalN  41172  djafvalN  41173  djhffval  41435  djhfval  41436  hlhilset  41973  eldiophb  42790  mendval  43212  mnringvald  44246  mnringmulrd  44256  hoidmvval  46615  ovnhoi  46641  hspval  46647  hspmbllem2  46665  hoimbl  46669  rngcvalALTV  48296  rngccoALTV  48302  ringcvalALTV  48320  ringccoALTV  48336  lincop  48440  lines  48763  rrxlines  48765  spheres  48778  invfn  49062  infsubc2  49093  imaidfu2  49143  upfval  49208  dfswapf2  49293  swapfval  49294  1stfpropd  49322  2ndfpropd  49323  fucofvalg  49350  fuco21  49368  precofval3  49403  prcofvalg  49408  setc1ocofval  49526  lanfval  49645  ranfval  49646