Theorem mpoeq123dv 7486

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149   ∈ cmpo 7413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-oprab 7415  df-mpo 7416

This theorem is referenced by:  mpoeq123i  7487  mptmpoopabbrd  8077  el2mpocsbcl  8079  bropopvvv  8084  bropfvvvv  8086  prdsval  17507  imasval  17564  imasvscaval  17591  homffval  17745  homfeq  17749  comfffval  17753  comffval  17754  comfffval2  17756  comffval2  17757  comfeq  17761  oppcval  17768  monfval  17788  sectffval  17806  invffval  17814  isofn  17831  cofuval  17938  natfval  18005  fucval  18017  fucco  18021  coafval  18120  setcval  18133  setcco  18139  catcval  18156  catcco  18161  estrcval  18179  estrcco  18185  xpcval  18232  1stfval  18246  2ndfval  18249  prfval  18254  evlfval  18272  evlf2  18273  curfval  18278  hofval  18307  hof2fval  18310  plusffval  18703  efmnd  18928  grpsubfval  19049  grpsubfvalALT  19050  grpsubpropd  19110  mulgfval  19134  mulgfvalALT  19135  mulgpropd  19181  lsmfval  19707  pj1fval  19763  efgtf  19791  prdsmgp  20226  dvrfval  20483  funcrngcsetcALT  20725  scaffval  20978  ipffval  21766  phssip  21776  frlmip  21896  psrval  22033  mamufval  22517  mvmulfval  22667  marrepfval  22685  marepvfval  22690  submafval  22704  submaval  22706  madufval  22762  minmar1fval  22771  mat2pmatfval  22848  cpm2mfval  22874  decpmatval0  22889  decpmatval  22890  pmatcollpw3lem  22908  xkoval  23712  xkopt  23780  xpstopnlem1  23934  submtmd  24229  blfvalps  24508  ishtpy  25099  isphtpy  25108  pcofval  25137  rrxip  25517  q1pval  26280  r1pval  26283  taylfval  26487  istrkgl  28692  tgplnfn  29014  plngval  29016  isplng  29017  midf  29042  ismidb  29044  ttgval  29164  wwlksnon  30140  wspthsnon  30141  clwwlknonmpo  30380  grpodivfval  30826  dipfval  30994  rlocval  33519  idlsrgval  33737  splyval  33893  submatres  34140  lmatval  34147  lmatcl  34150  qqhval  34306  sxval  34524  sitmval  34683  cndprobval  34767  mclsval  35953  csbfinxpg  37921  rrnval  38365  ldualset  39788  paddfval  40460  tgrpfset  41407  tgrpset  41408  erngfset  41462  erngset  41463  erngfset-rN  41470  erngset-rN  41471  dvafset  41667  dvaset  41668  dvhfset  41743  dvhset  41744  djaffvalN  41796  djafvalN  41797  djhffval  42059  djhfval  42060  hlhilset  42597  eldiophb  43379  mendval  43797  mnringvald  44828  mnringmulrd  44838  hoidmvval  47182  ovnhoi  47208  hspval  47214  hspmbllem2  47232  hoimbl  47236  rngcvalALTV  48918  rngccoALTV  48924  ringcvalALTV  48942  ringccoALTV  48958  lincop  49072  lines  49395  rrxlines  49397  spheres  49410  invfn  49692  infsubc2  49723  imaidfu2  49773  upfval  49838  dfswapf2  49923  swapfval  49924  1stfpropd  49952  2ndfpropd  49953  fucofvalg  49980  fuco21  49998  precofval3  50033  prcofvalg  50038  setc1ocofval  50156  lanfval  50275  ranfval  50276