Theorem mpoeq123dv 7497

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ∈ cmpo 7424

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-oprab 7426  df-mpo 7427

This theorem is used by:  mpoeq123i  7498  mptmpoopabbrd  8096  el2mpocsbcl  8098  bropopvvv  8103  bropfvvvv  8105  prdsval  17633  imasval  17690  imasvscaval  17717  homffval  17871  homfeq  17875  comfffval  17879  comffval  17880  comfffval2  17882  comffval2  17883  comfeq  17887  oppcval  17894  monfval  17914  sectffval  17932  invffval  17940  isofn  17957  cofuval  18064  natfval  18131  fucval  18143  fucco  18147  coafval  18246  setcval  18259  setcco  18265  catcval  18282  catcco  18287  estrcval  18305  estrcco  18311  xpcval  18358  1stfval  18372  2ndfval  18375  prfval  18380  evlfval  18398  evlf2  18399  curfval  18404  hofval  18433  hof2fval  18436  plusffval  18829  efmnd  19073  grpsubfval  19201  grpsubfvalALT  19202  grpsubpropd  19262  mulgfval  19286  mulgfvalALT  19287  mulgpropd  19333  lsmfval  19859  pj1fval  19915  efgtf  19943  prdsmgp  20378  dvrfval  20639  funcrngcsetcALT  20900  scaffval  21162  ipffval  21961  phssip  21971  frlmip  22091  psrval  22230  mamufval  22714  mvmulfval  22864  marrepfval  22882  marepvfval  22887  submafval  22901  submaval  22903  madufval  22959  minmar1fval  22968  mat2pmatfval  23048  cpm2mfval  23074  decpmatval0  23089  decpmatval  23090  pmatcollpw3lem  23108  xkoval  23913  xkopt  23981  xpstopnlem1  24135  submtmd  24430  blfvalps  24709  ishtpy  25300  isphtpy  25309  pcofval  25338  rrxip  25718  q1pval  26480  r1pval  26483  taylfval  26693  istrkgl  28927  tgplnfn  29260  plngval  29262  isplng  29263  midf  29288  ismidb  29290  angmgmval  29401  ttgval  29459  wwlksnon  30447  wspthsnon  30448  clwwlknonmpo  30687  grpodivfval  31143  dipfval  31311  rlocval  33868  idlsrgval  34083  splyval  34239  submatres  34486  lmatval  34493  lmatcl  34496  qqhval  34652  sxval  34871  sitmval  35029  cndprobval  35113  mclsval  36416  csbfinxpg  38418  rrnval  38868  ldualset  40289  paddfval  40961  tgrpfset  41908  tgrpset  41909  erngfset  41963  erngset  41964  erngfset-rN  41971  erngset-rN  41972  dvafset  42168  dvaset  42169  dvhfset  42244  dvhset  42245  djaffvalN  42297  djafvalN  42298  djhffval  42560  djhfval  42561  hlhilset  43098  eldiophb  43875  mendval  44288  mnringvald  45318  mnringmulrd  45328  hoidmvval  47694  ovnhoi  47720  hspval  47726  hspmbllem2  47744  hoimbl  47748  rngcvalALTV  49469  rngccoALTV  49475  ringcvalALTV  49493  ringccoALTV  49509  lincop  49627  lines  49951  rrxlines  49953  spheres  49965  invfn  50251  infsubc2  50282  imaidfu2  50334  upfval  50399  dfswapf2  50490  swapfval  50491  1stfpropd  50519  2ndfpropd  50520  fucofvalg  50547  fuco21  50565  precofval3  50613  prcofvalg  50618  setc1ocofval  50736  lanfval  50903  ranfval  50904