Theorem mpoeq123dv 7412

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540   ∈ wcel 2105   ∈ cmpo 7339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-oprab 7341  df-mpo 7342

This theorem is referenced by:  mpoeq123i  7413  mptmpoopabbrd  7989  mptmpoopabbrdOLD  7991  el2mpocsbcl  7993  bropopvvv  7998  bropfvvvv  8000  prdsval  17263  imasval  17319  imasvscaval  17346  homffval  17496  homfeq  17500  comfffval  17504  comffval  17505  comfffval2  17507  comffval2  17508  comfeq  17512  oppcval  17519  monfval  17541  sectffval  17559  invffval  17567  isofn  17584  cofuval  17694  natfval  17759  fucval  17772  fucco  17777  coafval  17876  setcval  17889  setcco  17895  catcval  17912  catcco  17917  estrcval  17937  estrcco  17943  xpcval  17991  1stfval  18005  2ndfval  18008  prfval  18013  evlfval  18032  evlf2  18033  curfval  18038  hofval  18067  hof2fval  18070  plusffval  18429  efmnd  18605  grpsubfval  18719  grpsubfvalALT  18720  grpsubpropd  18776  mulgfval  18798  mulgfvalALT  18799  mulgpropd  18841  lsmfval  19339  pj1fval  19395  efgtf  19423  prdsmgp  19944  dvrfval  20021  scaffval  20247  ipffval  20959  phssip  20969  frlmip  21091  psrval  21224  mamufval  21640  mvmulfval  21797  marrepfval  21815  marepvfval  21820  submafval  21834  submaval  21836  madufval  21892  minmar1fval  21901  mat2pmatfval  21978  cpm2mfval  22004  decpmatval0  22019  decpmatval  22020  pmatcollpw3lem  22038  xkoval  22844  xkopt  22912  xpstopnlem1  23066  submtmd  23361  blfvalps  23642  ishtpy  24241  isphtpy  24250  pcofval  24279  rrxip  24660  q1pval  25424  r1pval  25427  taylfval  25624  midf  27426  ismidb  27428  ttgval  27525  ttgvalOLD  27526  wwlksnon  28504  wspthsnon  28505  clwwlknonmpo  28741  grpodivfval  29184  dipfval  29352  idlsrgval  31945  submatres  32054  lmatval  32061  lmatcl  32064  qqhval  32222  sxval  32456  sitmval  32616  cndprobval  32700  mclsval  33824  csbfinxpg  35664  rrnval  36090  ldualset  37392  paddfval  38065  tgrpfset  39012  tgrpset  39013  erngfset  39067  erngset  39068  erngfset-rN  39075  erngset-rN  39076  dvafset  39272  dvaset  39273  dvhfset  39348  dvhset  39349  djaffvalN  39401  djafvalN  39402  djhffval  39664  djhfval  39665  hlhilset  40202  eldiophb  40841  mendval  41271  mnringvald  42147  mnringmulrd  42160  hoidmvval  44452  ovnhoi  44478  hspval  44484  hspmbllem2  44502  hoimbl  44506  rngcvalALTV  45870  rngccoALTV  45897  funcrngcsetcALT  45908  ringcvalALTV  45916  ringccoALTV  45960  lincop  46100  lines  46428  rrxlines  46430  spheres  46443