Theorem mpoeq123dv 7464

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

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

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 7391  df-mpo 7392

This theorem is referenced by:  mpoeq123i  7465  mptmpoopabbrd  8059  mptmpoopabbrdOLD  8060  mptmpoopabbrdOLDOLD  8062  el2mpocsbcl  8064  bropopvvv  8069  bropfvvvv  8071  prdsval  17418  imasval  17474  imasvscaval  17501  homffval  17651  homfeq  17655  comfffval  17659  comffval  17660  comfffval2  17662  comffval2  17663  comfeq  17667  oppcval  17674  monfval  17694  sectffval  17712  invffval  17720  isofn  17737  cofuval  17844  natfval  17911  fucval  17923  fucco  17927  coafval  18026  setcval  18039  setcco  18045  catcval  18062  catcco  18067  estrcval  18085  estrcco  18091  xpcval  18138  1stfval  18152  2ndfval  18155  prfval  18160  evlfval  18178  evlf2  18179  curfval  18184  hofval  18213  hof2fval  18216  plusffval  18573  efmnd  18797  grpsubfval  18915  grpsubfvalALT  18916  grpsubpropd  18977  mulgfval  19001  mulgfvalALT  19002  mulgpropd  19048  lsmfval  19568  pj1fval  19624  efgtf  19652  prdsmgp  20060  dvrfval  20311  funcrngcsetcALT  20550  scaffval  20786  ipffval  21557  phssip  21567  frlmip  21687  psrval  21824  mamufval  22279  mvmulfval  22429  marrepfval  22447  marepvfval  22452  submafval  22466  submaval  22468  madufval  22524  minmar1fval  22533  mat2pmatfval  22610  cpm2mfval  22636  decpmatval0  22651  decpmatval  22652  pmatcollpw3lem  22670  xkoval  23474  xkopt  23542  xpstopnlem1  23696  submtmd  23991  blfvalps  24271  ishtpy  24871  isphtpy  24880  pcofval  24910  rrxip  25290  q1pval  26060  r1pval  26063  taylfval  26266  istrkgl  28385  midf  28703  ismidb  28705  ttgval  28802  wwlksnon  29781  wspthsnon  29782  clwwlknonmpo  30018  grpodivfval  30463  dipfval  30631  rlocval  33210  idlsrgval  33474  submatres  33796  lmatval  33803  lmatcl  33806  qqhval  33962  sxval  34180  sitmval  34340  cndprobval  34424  mclsval  35550  csbfinxpg  37376  rrnval  37821  ldualset  39118  paddfval  39791  tgrpfset  40738  tgrpset  40739  erngfset  40793  erngset  40794  erngfset-rN  40801  erngset-rN  40802  dvafset  40998  dvaset  40999  dvhfset  41074  dvhset  41075  djaffvalN  41127  djafvalN  41128  djhffval  41390  djhfval  41391  hlhilset  41928  eldiophb  42745  mendval  43168  mnringvald  44202  mnringmulrd  44212  hoidmvval  46575  ovnhoi  46601  hspval  46607  hspmbllem2  46625  hoimbl  46629  rngcvalALTV  48253  rngccoALTV  48259  ringcvalALTV  48277  ringccoALTV  48293  lincop  48397  lines  48720  rrxlines  48722  spheres  48735  invfn  49019  infsubc2  49050  imaidfu2  49100  upfval  49165  dfswapf2  49250  swapfval  49251  1stfpropd  49279  2ndfpropd  49280  fucofvalg  49307  fuco21  49325  precofval3  49360  prcofvalg  49365  setc1ocofval  49483  lanfval  49602  ranfval  49603