Theorem mpoeq123dv 7494

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146   ∈ cmpo 7421

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-oprab 7423  df-mpo 7424

This theorem is used by:  mpoeq123i  7495  mptmpoopabbrd  8084  el2mpocsbcl  8086  bropopvvv  8091  bropfvvvv  8093  prdsval  17530  imasval  17587  imasvscaval  17614  homffval  17768  homfeq  17772  comfffval  17776  comffval  17777  comfffval2  17779  comffval2  17780  comfeq  17784  oppcval  17791  monfval  17811  sectffval  17829  invffval  17837  isofn  17854  cofuval  17961  natfval  18028  fucval  18040  fucco  18044  coafval  18143  setcval  18156  setcco  18162  catcval  18179  catcco  18184  estrcval  18202  estrcco  18208  xpcval  18255  1stfval  18269  2ndfval  18272  prfval  18277  evlfval  18295  evlf2  18296  curfval  18301  hofval  18330  hof2fval  18333  plusffval  18726  efmnd  18966  grpsubfval  19094  grpsubfvalALT  19095  grpsubpropd  19155  mulgfval  19179  mulgfvalALT  19180  mulgpropd  19226  lsmfval  19752  pj1fval  19808  efgtf  19836  prdsmgp  20271  dvrfval  20530  funcrngcsetcALT  20790  scaffval  21051  ipffval  21848  phssip  21858  frlmip  21978  psrval  22115  mamufval  22599  mvmulfval  22749  marrepfval  22767  marepvfval  22772  submafval  22786  submaval  22788  madufval  22844  minmar1fval  22853  mat2pmatfval  22930  cpm2mfval  22956  decpmatval0  22971  decpmatval  22972  pmatcollpw3lem  22990  xkoval  23795  xkopt  23863  xpstopnlem1  24017  submtmd  24312  blfvalps  24591  ishtpy  25182  isphtpy  25191  pcofval  25220  rrxip  25600  q1pval  26363  r1pval  26366  taylfval  26573  istrkgl  28778  tgplnfn  29108  plngval  29110  isplng  29111  midf  29136  ismidb  29138  ttgval  29279  wwlksnon  30267  wspthsnon  30268  clwwlknonmpo  30507  grpodivfval  30957  dipfval  31125  rlocval  33643  idlsrgval  33857  splyval  34013  submatres  34260  lmatval  34267  lmatcl  34270  qqhval  34426  sxval  34645  sitmval  34804  cndprobval  34888  mclsval  36092  csbfinxpg  38091  rrnval  38536  ldualset  39957  paddfval  40629  tgrpfset  41576  tgrpset  41577  erngfset  41631  erngset  41632  erngfset-rN  41639  erngset-rN  41640  dvafset  41836  dvaset  41837  dvhfset  41912  dvhset  41913  djaffvalN  41965  djafvalN  41966  djhffval  42228  djhfval  42229  hlhilset  42766  eldiophb  43546  mendval  43964  mnringvald  44995  mnringmulrd  45005  hoidmvval  47349  ovnhoi  47375  hspval  47381  hspmbllem2  47399  hoimbl  47403  rngcvalALTV  49087  rngccoALTV  49093  ringcvalALTV  49111  ringccoALTV  49127  lincop  49245  lines  49568  rrxlines  49570  spheres  49583  invfn  49865  infsubc2  49896  imaidfu2  49946  upfval  50011  dfswapf2  50096  swapfval  50097  1stfpropd  50125  2ndfpropd  50126  fucofvalg  50153  fuco21  50171  precofval3  50206  prcofvalg  50211  setc1ocofval  50329  lanfval  50448  ranfval  50449