Theorem mpoeq123dv 7443

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ∈ cmpo 7370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-oprab 7372  df-mpo 7373

This theorem is referenced by:  mpoeq123i  7444  mptmpoopabbrd  8034  mptmpoopabbrdOLD  8035  el2mpocsbcl  8037  bropopvvv  8042  bropfvvvv  8044  prdsval  17387  imasval  17444  imasvscaval  17471  homffval  17625  homfeq  17629  comfffval  17633  comffval  17634  comfffval2  17636  comffval2  17637  comfeq  17641  oppcval  17648  monfval  17668  sectffval  17686  invffval  17694  isofn  17711  cofuval  17818  natfval  17885  fucval  17897  fucco  17901  coafval  18000  setcval  18013  setcco  18019  catcval  18036  catcco  18041  estrcval  18059  estrcco  18065  xpcval  18112  1stfval  18126  2ndfval  18129  prfval  18134  evlfval  18152  evlf2  18153  curfval  18158  hofval  18187  hof2fval  18190  plusffval  18583  efmnd  18807  grpsubfval  18925  grpsubfvalALT  18926  grpsubpropd  18987  mulgfval  19011  mulgfvalALT  19012  mulgpropd  19058  lsmfval  19579  pj1fval  19635  efgtf  19663  prdsmgp  20098  dvrfval  20350  funcrngcsetcALT  20586  scaffval  20843  ipffval  21615  phssip  21625  frlmip  21745  psrval  21883  mamufval  22348  mvmulfval  22498  marrepfval  22516  marepvfval  22521  submafval  22535  submaval  22537  madufval  22593  minmar1fval  22602  mat2pmatfval  22679  cpm2mfval  22705  decpmatval0  22720  decpmatval  22721  pmatcollpw3lem  22739  xkoval  23543  xkopt  23611  xpstopnlem1  23765  submtmd  24060  blfvalps  24339  ishtpy  24939  isphtpy  24948  pcofval  24978  rrxip  25358  q1pval  26128  r1pval  26131  taylfval  26334  istrkgl  28542  midf  28860  ismidb  28862  ttgval  28959  wwlksnon  29936  wspthsnon  29937  clwwlknonmpo  30176  grpodivfval  30622  dipfval  30790  rlocval  33353  idlsrgval  33596  splyval  33736  submatres  33984  lmatval  33991  lmatcl  33994  qqhval  34150  sxval  34368  sitmval  34527  cndprobval  34611  mclsval  35779  csbfinxpg  37643  rrnval  38078  ldualset  39501  paddfval  40173  tgrpfset  41120  tgrpset  41121  erngfset  41175  erngset  41176  erngfset-rN  41183  erngset-rN  41184  dvafset  41380  dvaset  41381  dvhfset  41456  dvhset  41457  djaffvalN  41509  djafvalN  41510  djhffval  41772  djhfval  41773  hlhilset  42310  eldiophb  43114  mendval  43536  mnringvald  44569  mnringmulrd  44579  hoidmvval  46935  ovnhoi  46961  hspval  46967  hspmbllem2  46985  hoimbl  46989  rngcvalALTV  48625  rngccoALTV  48631  ringcvalALTV  48649  ringccoALTV  48665  lincop  48768  lines  49091  rrxlines  49093  spheres  49106  invfn  49389  infsubc2  49420  imaidfu2  49470  upfval  49535  dfswapf2  49620  swapfval  49621  1stfpropd  49649  2ndfpropd  49650  fucofvalg  49677  fuco21  49695  precofval3  49730  prcofvalg  49735  setc1ocofval  49853  lanfval  49972  ranfval  49973