Theorem mpoeq123dv 7087

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522   ∈ wcel 2081   ∈ cmpo 7018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-oprab 7020  df-mpo 7021

This theorem is referenced by:  mpoeq123i  7088  mptmpoopabbrd  7634  el2mpocsbcl  7636  bropopvvv  7641  bropfvvvv  7643  prdsval  16557  imasval  16613  imasvscaval  16640  homffval  16789  homfeq  16793  comfffval  16797  comffval  16798  comfffval2  16800  comffval2  16801  comfeq  16805  oppcval  16812  monfval  16831  sectffval  16849  invffval  16857  isofn  16874  cofuval  16981  natfval  17045  fucval  17057  fucco  17061  coafval  17153  setcval  17166  setcco  17172  catcval  17185  catcco  17190  estrcval  17203  estrcco  17209  xpcval  17256  xpchomfval  17258  xpccofval  17261  1stfval  17270  2ndfval  17273  prfval  17278  evlfval  17296  evlf2  17297  curfval  17302  hofval  17331  hof2fval  17334  plusffval  17686  grpsubfval  17904  grpsubfvalALT  17905  grpsubpropd  17961  mulgfval  17983  mulgfvalALT  17984  mulgpropd  18023  symgval  18238  lsmfval  18493  pj1fval  18547  efgtf  18575  prdsmgp  19050  dvrfval  19124  scaffval  19342  psrval  19830  ipffval  20474  phssip  20484  frlmip  20604  mamufval  20678  mvmulfval  20835  marrepfval  20853  marepvfval  20858  submafval  20872  submaval  20874  madufval  20930  minmar1fval  20939  mat2pmatfval  21015  cpm2mfval  21041  decpmatval0  21056  decpmatval  21057  pmatcollpw3lem  21075  xkoval  21879  xkopt  21947  xpstopnlem1  22101  submtmd  22396  blfvalps  22676  ishtpy  23259  isphtpy  23268  pcofval  23297  rrxip  23676  q1pval  24430  r1pval  24433  taylfval  24630  midf  26244  ismidb  26246  ttgval  26344  wwlksnon  27316  wspthsnon  27317  clwwlknonmpo  27555  grpodivfval  28002  dipfval  28170  submatres  30686  lmatval  30693  lmatcl  30696  qqhval  30832  sxval  31066  sitmval  31224  cndprobval  31308  mclsval  32419  csbfinxpg  34219  rrnval  34656  ldualset  35811  paddfval  36483  tgrpfset  37430  tgrpset  37431  erngfset  37485  erngset  37486  erngfset-rN  37493  erngset-rN  37494  dvafset  37690  dvaset  37691  dvhfset  37766  dvhset  37767  djaffvalN  37819  djafvalN  37820  djhffval  38082  djhfval  38083  hlhilset  38620  eldiophb  38858  mendval  39287  hoidmvval  42421  ovnhoi  42447  hspval  42453  hspmbllem2  42471  hoimbl  42475  rngcvalALTV  43730  rngccoALTV  43757  funcrngcsetcALT  43768  ringcvalALTV  43776  ringccoALTV  43820  lincop  43963  lines  44219  rrxlines  44221  spheres  44234