Theorem mpoeq123dv 7444

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ∈ cmpo 7371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-oprab 7373  df-mpo 7374

This theorem is referenced by:  mpoeq123i  7445  mptmpoopabbrd  8038  mptmpoopabbrdOLD  8039  el2mpocsbcl  8041  bropopvvv  8046  bropfvvvv  8048  prdsval  17394  imasval  17450  imasvscaval  17477  homffval  17627  homfeq  17631  comfffval  17635  comffval  17636  comfffval2  17638  comffval2  17639  comfeq  17643  oppcval  17650  monfval  17670  sectffval  17688  invffval  17696  isofn  17713  cofuval  17820  natfval  17887  fucval  17899  fucco  17903  coafval  18002  setcval  18015  setcco  18021  catcval  18038  catcco  18043  estrcval  18061  estrcco  18067  xpcval  18114  1stfval  18128  2ndfval  18131  prfval  18136  evlfval  18154  evlf2  18155  curfval  18160  hofval  18189  hof2fval  18192  plusffval  18549  efmnd  18773  grpsubfval  18891  grpsubfvalALT  18892  grpsubpropd  18953  mulgfval  18977  mulgfvalALT  18978  mulgpropd  19024  lsmfval  19544  pj1fval  19600  efgtf  19628  prdsmgp  20036  dvrfval  20287  funcrngcsetcALT  20526  scaffval  20762  ipffval  21533  phssip  21543  frlmip  21663  psrval  21800  mamufval  22255  mvmulfval  22405  marrepfval  22423  marepvfval  22428  submafval  22442  submaval  22444  madufval  22500  minmar1fval  22509  mat2pmatfval  22586  cpm2mfval  22612  decpmatval0  22627  decpmatval  22628  pmatcollpw3lem  22646  xkoval  23450  xkopt  23518  xpstopnlem1  23672  submtmd  23967  blfvalps  24247  ishtpy  24847  isphtpy  24856  pcofval  24886  rrxip  25266  q1pval  26036  r1pval  26039  taylfval  26242  istrkgl  28361  midf  28679  ismidb  28681  ttgval  28778  wwlksnon  29754  wspthsnon  29755  clwwlknonmpo  29991  grpodivfval  30436  dipfval  30604  rlocval  33183  idlsrgval  33447  submatres  33769  lmatval  33776  lmatcl  33779  qqhval  33935  sxval  34153  sitmval  34313  cndprobval  34397  mclsval  35523  csbfinxpg  37349  rrnval  37794  ldualset  39091  paddfval  39764  tgrpfset  40711  tgrpset  40712  erngfset  40766  erngset  40767  erngfset-rN  40774  erngset-rN  40775  dvafset  40971  dvaset  40972  dvhfset  41047  dvhset  41048  djaffvalN  41100  djafvalN  41101  djhffval  41363  djhfval  41364  hlhilset  41901  eldiophb  42718  mendval  43141  mnringvald  44175  mnringmulrd  44185  hoidmvval  46548  ovnhoi  46574  hspval  46580  hspmbllem2  46598  hoimbl  46602  rngcvalALTV  48226  rngccoALTV  48232  ringcvalALTV  48250  ringccoALTV  48266  lincop  48370  lines  48693  rrxlines  48695  spheres  48708  invfn  48992  infsubc2  49023  imaidfu2  49073  upfval  49138  dfswapf2  49223  swapfval  49224  1stfpropd  49252  2ndfpropd  49253  fucofvalg  49280  fuco21  49298  precofval3  49333  prcofvalg  49338  setc1ocofval  49456  lanfval  49575  ranfval  49576