Theorem mpoeq123dv 7286

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2110   ∈ cmpo 7215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-12 2175  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-oprab 7217  df-mpo 7218

This theorem is referenced by:  mpoeq123i  7287  mptmpoopabbrd  7851  el2mpocsbcl  7853  bropopvvv  7858  bropfvvvv  7860  prdsval  16960  imasval  17016  imasvscaval  17043  homffval  17193  homfeq  17197  comfffval  17201  comffval  17202  comfffval2  17204  comffval2  17205  comfeq  17209  oppcval  17216  monfval  17237  sectffval  17255  invffval  17263  isofn  17280  cofuval  17388  natfval  17453  fucval  17466  fucco  17471  coafval  17570  setcval  17583  setcco  17589  catcval  17606  catcco  17611  estrcval  17631  estrcco  17637  xpcval  17684  1stfval  17698  2ndfval  17701  prfval  17706  evlfval  17725  evlf2  17726  curfval  17731  hofval  17760  hof2fval  17763  plusffval  18120  efmnd  18297  grpsubfval  18411  grpsubfvalALT  18412  grpsubpropd  18468  mulgfval  18490  mulgfvalALT  18491  mulgpropd  18533  lsmfval  19027  pj1fval  19084  efgtf  19112  prdsmgp  19628  dvrfval  19702  scaffval  19917  ipffval  20610  phssip  20620  frlmip  20740  psrval  20874  mamufval  21284  mvmulfval  21439  marrepfval  21457  marepvfval  21462  submafval  21476  submaval  21478  madufval  21534  minmar1fval  21543  mat2pmatfval  21620  cpm2mfval  21646  decpmatval0  21661  decpmatval  21662  pmatcollpw3lem  21680  xkoval  22484  xkopt  22552  xpstopnlem1  22706  submtmd  23001  blfvalps  23281  ishtpy  23869  isphtpy  23878  pcofval  23907  rrxip  24287  q1pval  25051  r1pval  25054  taylfval  25251  midf  26867  ismidb  26869  ttgval  26966  wwlksnon  27935  wspthsnon  27936  clwwlknonmpo  28172  grpodivfval  28615  dipfval  28783  idlsrgval  31362  submatres  31470  lmatval  31477  lmatcl  31480  qqhval  31636  sxval  31870  sitmval  32028  cndprobval  32112  mclsval  33238  csbfinxpg  35296  rrnval  35722  ldualset  36876  paddfval  37548  tgrpfset  38495  tgrpset  38496  erngfset  38550  erngset  38551  erngfset-rN  38558  erngset-rN  38559  dvafset  38755  dvaset  38756  dvhfset  38831  dvhset  38832  djaffvalN  38884  djafvalN  38885  djhffval  39147  djhfval  39148  hlhilset  39685  eldiophb  40282  mendval  40711  mnringvald  41504  mnringmulrd  41514  hoidmvval  43790  ovnhoi  43816  hspval  43822  hspmbllem2  43840  hoimbl  43844  rngcvalALTV  45192  rngccoALTV  45219  funcrngcsetcALT  45230  ringcvalALTV  45238  ringccoALTV  45282  lincop  45422  lines  45750  rrxlines  45752  spheres  45765