Theorem mpoeq123dv 7507

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105   ∈ cmpo 7432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-oprab 7434  df-mpo 7435

This theorem is referenced by:  mpoeq123i  7508  mptmpoopabbrd  8103  mptmpoopabbrdOLD  8104  mptmpoopabbrdOLDOLD  8106  el2mpocsbcl  8108  bropopvvv  8113  bropfvvvv  8115  prdsval  17501  imasval  17557  imasvscaval  17584  homffval  17734  homfeq  17738  comfffval  17742  comffval  17743  comfffval2  17745  comffval2  17746  comfeq  17750  oppcval  17757  monfval  17779  sectffval  17797  invffval  17805  isofn  17822  cofuval  17932  natfval  18000  fucval  18013  fucco  18018  coafval  18117  setcval  18130  setcco  18136  catcval  18153  catcco  18158  estrcval  18178  estrcco  18184  xpcval  18232  1stfval  18246  2ndfval  18249  prfval  18254  evlfval  18273  evlf2  18274  curfval  18279  hofval  18308  hof2fval  18311  plusffval  18671  efmnd  18895  grpsubfval  19013  grpsubfvalALT  19014  grpsubpropd  19075  mulgfval  19099  mulgfvalALT  19100  mulgpropd  19146  lsmfval  19670  pj1fval  19726  efgtf  19754  prdsmgp  20168  dvrfval  20418  funcrngcsetcALT  20657  scaffval  20894  ipffval  21683  phssip  21693  frlmip  21815  psrval  21952  mamufval  22411  mvmulfval  22563  marrepfval  22581  marepvfval  22586  submafval  22600  submaval  22602  madufval  22658  minmar1fval  22667  mat2pmatfval  22744  cpm2mfval  22770  decpmatval0  22785  decpmatval  22786  pmatcollpw3lem  22804  xkoval  23610  xkopt  23678  xpstopnlem1  23832  submtmd  24127  blfvalps  24408  ishtpy  25017  isphtpy  25026  pcofval  25056  rrxip  25437  q1pval  26208  r1pval  26211  taylfval  26414  istrkgl  28480  midf  28798  ismidb  28800  ttgval  28897  ttgvalOLD  28898  wwlksnon  29880  wspthsnon  29881  clwwlknonmpo  30117  grpodivfval  30562  dipfval  30730  rlocval  33245  idlsrgval  33510  submatres  33766  lmatval  33773  lmatcl  33776  qqhval  33934  sxval  34170  sitmval  34330  cndprobval  34414  mclsval  35547  csbfinxpg  37370  rrnval  37813  ldualset  39106  paddfval  39779  tgrpfset  40726  tgrpset  40727  erngfset  40781  erngset  40782  erngfset-rN  40789  erngset-rN  40790  dvafset  40986  dvaset  40987  dvhfset  41062  dvhset  41063  djaffvalN  41115  djafvalN  41116  djhffval  41378  djhfval  41379  hlhilset  41916  eldiophb  42744  mendval  43167  mnringvald  44203  mnringmulrd  44216  hoidmvval  46532  ovnhoi  46558  hspval  46564  hspmbllem2  46582  hoimbl  46586  rngcvalALTV  48108  rngccoALTV  48114  ringcvalALTV  48132  ringccoALTV  48148  lincop  48253  lines  48580  rrxlines  48582  spheres  48595