Theorem mpoeq123dv 7466

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141   ∈ cmpo 7393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-oprab 7395  df-mpo 7396

This theorem is referenced by:  mpoeq123i  7467  mptmpoopabbrd  8056  el2mpocsbcl  8058  bropopvvv  8063  bropfvvvv  8065  prdsval  17475  imasval  17532  imasvscaval  17559  homffval  17713  homfeq  17717  comfffval  17721  comffval  17722  comfffval2  17724  comffval2  17725  comfeq  17729  oppcval  17736  monfval  17756  sectffval  17774  invffval  17782  isofn  17799  cofuval  17906  natfval  17973  fucval  17985  fucco  17989  coafval  18088  setcval  18101  setcco  18107  catcval  18124  catcco  18129  estrcval  18147  estrcco  18153  xpcval  18200  1stfval  18214  2ndfval  18217  prfval  18222  evlfval  18240  evlf2  18241  curfval  18246  hofval  18275  hof2fval  18278  plusffval  18671  efmnd  18895  grpsubfval  19016  grpsubfvalALT  19017  grpsubpropd  19078  mulgfval  19102  mulgfvalALT  19103  mulgpropd  19149  lsmfval  19669  pj1fval  19725  efgtf  19753  prdsmgp  20188  dvrfval  20438  funcrngcsetcALT  20678  scaffval  20935  ipffval  21688  phssip  21698  frlmip  21818  psrval  21955  mamufval  22440  mvmulfval  22590  marrepfval  22608  marepvfval  22613  submafval  22627  submaval  22629  madufval  22685  minmar1fval  22694  mat2pmatfval  22771  cpm2mfval  22797  decpmatval0  22812  decpmatval  22813  pmatcollpw3lem  22831  xkoval  23635  xkopt  23703  xpstopnlem1  23857  submtmd  24152  blfvalps  24431  ishtpy  25022  isphtpy  25031  pcofval  25060  rrxip  25440  q1pval  26203  r1pval  26206  taylfval  26410  istrkgl  28615  midf  28933  ismidb  28935  ttgval  29032  wwlksnon  30008  wspthsnon  30009  clwwlknonmpo  30248  grpodivfval  30694  dipfval  30862  rlocval  33401  idlsrgval  33660  splyval  33817  submatres  34064  lmatval  34071  lmatcl  34074  qqhval  34230  sxval  34448  sitmval  34607  cndprobval  34691  mclsval  35874  csbfinxpg  37843  rrnval  38287  ldualset  39710  paddfval  40382  tgrpfset  41329  tgrpset  41330  erngfset  41384  erngset  41385  erngfset-rN  41392  erngset-rN  41393  dvafset  41589  dvaset  41590  dvhfset  41665  dvhset  41666  djaffvalN  41718  djafvalN  41719  djhffval  41981  djhfval  41982  hlhilset  42519  eldiophb  43299  mendval  43717  mnringvald  44750  mnringmulrd  44760  hoidmvval  47112  ovnhoi  47138  hspval  47144  hspmbllem2  47162  hoimbl  47166  rngcvalALTV  48848  rngccoALTV  48854  ringcvalALTV  48872  ringccoALTV  48888  lincop  48991  lines  49314  rrxlines  49316  spheres  49329  invfn  49612  infsubc2  49643  imaidfu2  49693  upfval  49758  dfswapf2  49843  swapfval  49844  1stfpropd  49872  2ndfpropd  49873  fucofvalg  49900  fuco21  49918  precofval3  49953  prcofvalg  49958  setc1ocofval  50076  lanfval  50195  ranfval  50196