MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvmptd Structured version   Visualization version   GIF version

Theorem fvmptd 6327
Description: Deduction version of fvmpt 6321. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypotheses
Ref Expression
fvmptd.1 (𝜑𝐹 = (𝑥𝐷𝐵))
fvmptd.2 ((𝜑𝑥 = 𝐴) → 𝐵 = 𝐶)
fvmptd.3 (𝜑𝐴𝐷)
fvmptd.4 (𝜑𝐶𝑉)
Assertion
Ref Expression
fvmptd (𝜑 → (𝐹𝐴) = 𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷   𝜑,𝑥
Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem fvmptd
StepHypRef Expression
1 fvmptd.1 . . 3 (𝜑𝐹 = (𝑥𝐷𝐵))
21fveq1d 6231 . 2 (𝜑 → (𝐹𝐴) = ((𝑥𝐷𝐵)‘𝐴))
3 fvmptd.3 . . 3 (𝜑𝐴𝐷)
4 fvmptd.2 . . . . 5 ((𝜑𝑥 = 𝐴) → 𝐵 = 𝐶)
53, 4csbied 3593 . . . 4 (𝜑𝐴 / 𝑥𝐵 = 𝐶)
6 fvmptd.4 . . . 4 (𝜑𝐶𝑉)
75, 6eqeltrd 2730 . . 3 (𝜑𝐴 / 𝑥𝐵𝑉)
8 eqid 2651 . . . 4 (𝑥𝐷𝐵) = (𝑥𝐷𝐵)
98fvmpts 6324 . . 3 ((𝐴𝐷𝐴 / 𝑥𝐵𝑉) → ((𝑥𝐷𝐵)‘𝐴) = 𝐴 / 𝑥𝐵)
103, 7, 9syl2anc 694 . 2 (𝜑 → ((𝑥𝐷𝐵)‘𝐴) = 𝐴 / 𝑥𝐵)
112, 10, 53eqtrd 2689 1 (𝜑 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wcel 2030  csb 3566  cmpt 4762  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-iota 5889  df-fun 5928  df-fv 5934
This theorem is referenced by:  fvmptdv2  6337  fvmptopab  6739  mptmpt2opabbrd  7293  bropfvvvv  7302  mpt2curryvald  7441  ttukeylem3  9371  ccatval1  13395  ccatval2  13396  repswsymb  13567  relexp1g  13810  rtrclreclem2  13843  rtrclreclem4  13845  dfrtrcl2  13846  lcmfval  15381  lcmf0val  15382  prmoval  15784  fvprmselelfz  15795  fvprmselgcd1  15796  prmodvdslcmf  15798  prmgap  15810  prmgaplcm  15811  prmgapprmo  15813  prdsvscafval  16187  mrcval  16317  cidval  16385  isofval  16464  isofn  16482  cicfval  16504  subcid  16554  idfu2nd  16584  resf2nd  16602  fuccoval  16670  fucid  16678  initoval  16694  termoval  16695  zerooval  16696  homaval  16728  idaval  16755  setcval  16774  setcid  16783  catcval  16793  catcid  16800  estrcval  16811  estrcid  16821  funcestrcsetclem1  16827  funcsetcestrclem1  16841  prf1  16887  prf2  16889  curf1  16912  curf11  16913  curf2val  16917  hofval  16939  hof2  16944  yonval  16948  yonedalem4a  16962  frmdval  17435  vrmdval  17441  pmtrdifwrdellem3  17949  gexval  18039  pj1val  18154  dpjval  18501  sraval  19224  opsrval  19522  cply1mul  19712  cply1coe0  19717  cply1coe0bi  19718  gsummoncoe1  19722  evls1sca  19736  frlmphl  20168  mat1rhmval  20333  scmatrhmval  20381  mvmulfv  20398  mavmulfv  20400  mdetuni0  20475  mat2pmatval  20577  m2cpm  20594  cpm2mval  20603  m2cpminvid2lem  20607  decpmatid  20623  decpmatmullem  20624  pmatcollpw2lem  20630  monmatcollpw  20632  pmatcollpw3fi1lem1  20639  pm2mpfval  20649  mply1topmatval  20657  mp2pm2mplem1  20659  mp2pm2mplem4  20662  pm2mpmhmlem2  20672  chpmatval  20684  chfacfscmul0  20711  chfacfscmulgsum  20713  chfacfpmmul0  20715  chfacfpmmulgsum  20717  lmfval  21084  kgenval  21386  ptval  21421  fcfval  21884  cnextfval  21913  ustval  22053  utopval  22083  ustuqtoplem  22090  utopsnneiplem  22098  tusval  22117  blfvalps  22235  tmsval  22333  metuval  22401  caufval  23119  rrxmvallem  23233  rrxmval  23234  taylpval  24166  efgh  24332  lgamgulmlem2  24801  lgamcvglem  24811  logexprlim  24995  dchrval  25004  dchr1  25027  gausslemma2dlem2  25137  gausslemma2dlem3  25138  gausslemma2dlem4  25139  2lgslem1b  25162  ishlg  25542  mirval  25595  mirfv  25596  israg  25637  perpln1  25650  perpln2  25651  isperp  25652  ishpg  25696  midf  25713  ismidb  25715  lmif  25722  islmib  25724  edgval  25986  edgvalOLD  25987  uvtxavalOLD  26334  vtxdgfval  26419  wksfval  26561  crctcshwlkn0lem2  26759  crctcshwlkn0lem3  26760  crctcsh  26772  wwlks  26783  wlkiswwlks2lem2  26824  wlkpwwlkf1ouspgr  26833  clwwlk  26951  clwlkclwwlklem2fv1  26961  clwlkclwwlklem2fv2  26962  numclwlk2lem2fv  27358  numclwlk2lem2fvOLD  27365  sgnsval  29856  psgnfzto1stlem  29978  fzto1stfv1  29979  madjusmdetlem2  30022  metidval  30061  pstmval  30066  qqhvval  30155  indv  30202  indval  30203  indfval  30206  esummulc1  30271  esumcvg  30276  ofcval  30289  sigagenval  30331  measinb  30412  omsval  30483  omsfval  30484  omssubadd  30490  carsgval  30493  sitgfval  30531  eulerpartlemsv1  30546  eulerpartlems  30550  eulerpartlemgvv  30566  fibp1  30591  totprobd  30616  probmeasb  30620  cndprobval  30623  dstrvprob  30661  dstfrvinc  30666  dstfrvclim1  30667  ballotlemfval  30679  ballotlemsv  30699  gsumnunsn  30743  signsply0  30756  signstfval  30769  fdvneggt  30806  fdvnegge  30808  itgexpif  30812  reprval  30816  breprexplema  30836  vtsval  30843  logdivsqrle  30856  hgt750lemg  30860  hgt750lemb  30862  afsval  30877  cvmliftlem9  31401  mvrsval  31528  mrsubfval  31531  mrsubval  31532  msubfval  31547  msubval  31548  msrval  31561  fwddifval  32394  fwddifnval  32395  knoppcnlem1  32608  knoppcnlem4  32611  knoppcnlem6  32613  knoppcnlem7  32614  knoppcnlem9  32616  unbdqndv2lem2  32626  knoppndvlem4  32631  knoppndvlem6  32633  bj-finsumval0  33277  poimirlem1  33540  poimirlem2  33541  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem19  33558  poimirlem22  33561  mblfinlem2  33577  areacirc  33635  cdleme31fv2  35998  tendopl2  36382  tendoi2  36400  erngplus2  36409  erngplus2-rN  36417  hlhilset  37543  itgpowd  38117  iunrelexpmin1  38317  iunrelexpmin2  38321  rfovfvd  38613  rfovfvfvd  38614  rfovcnvf1od  38615  rfovcnvfvd  38618  fsovfvd  38621  fsovfvfvd  38622  fsovcnvlem  38624  dssmapfvd  38628  dssmapfv2d  38629  dssmapfv3d  38630  dssmapnvod  38631  clsk3nimkb  38655  dvgrat  38828  radcnvrat  38830  hashnzfzclim  38838  binomcxplemnn0  38865  binomcxplemrat  38866  binomcxplemfrat  38867  binomcxplemradcnv  38868  binomcxplemcvg  38870  binomcxplemdvsum  38871  binomcxplemnotnn0  38872  projf1o  39700  mapss2  39711  fvmptd2  39759  fmuldfeqlem1  40132  clim1fr1  40151  climrec  40153  climexp  40155  climneg  40160  mullimcf  40173  divcnvg  40177  sumnnodd  40180  expfac  40207  fnlimfv  40213  fnlimabslt  40229  supcnvlimsup  40290  cncfshift  40405  icccncfext  40418  cncfioobdlem  40427  fprodsubrecnncnvlem  40439  fprodaddrecnncnvlem  40441  dvsinax  40445  fperdvper  40451  dvcosax  40459  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnmul  40476  dvnprodlem1  40479  dvnprodlem2  40480  dvnprodlem3  40481  itgsinexp  40488  itgcoscmulx  40503  itgsincmulx  40508  itgsubsticclem  40509  itgsubsticc  40510  itgiccshift  40514  stoweidlem7  40542  stoweidlem17  40552  stoweidlem32  40567  stoweidlem34  40569  wallispilem4  40603  wallispilem5  40604  wallispi  40605  wallispi2lem1  40606  wallispi2lem2  40607  wallispi2  40608  stirlinglem1  40609  stirlinglem2  40610  stirlinglem3  40611  stirlinglem4  40612  stirlinglem5  40613  stirlinglem7  40615  stirlinglem8  40616  stirlinglem10  40618  stirlinglem11  40619  stirlinglem12  40620  stirlinglem13  40621  stirlinglem14  40622  stirlinglem15  40623  dirkerval2  40629  dirkercncflem2  40639  fourierdlem7  40649  fourierdlem13  40655  fourierdlem14  40656  fourierdlem16  40658  fourierdlem18  40660  fourierdlem19  40661  fourierdlem21  40663  fourierdlem22  40664  fourierdlem26  40668  fourierdlem37  40679  fourierdlem39  40681  fourierdlem41  40683  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem51  40692  fourierdlem53  40694  fourierdlem62  40703  fourierdlem63  40704  fourierdlem65  40706  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem79  40720  fourierdlem81  40722  fourierdlem82  40723  fourierdlem83  40724  fourierdlem84  40725  fourierdlem88  40729  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem92  40733  fourierdlem93  40734  fourierdlem97  40738  fourierdlem101  40742  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem112  40753  fouriersw  40766  elaa2lem  40768  etransclem1  40770  etransclem12  40781  etransclem13  40782  etransclem17  40786  etransclem18  40787  etransclem21  40790  etransclem27  40796  etransclem31  40800  etransclem32  40801  etransclem33  40802  etransclem35  40804  etransclem46  40815  etransclem48  40817  rrxtopnfi  40824  salgenval  40859  sge0val  40901  sge0z  40910  sge0snmpt  40918  sge0xp  40964  nnfoctbdjlem  40990  psmeasurelem  41005  psmeasure  41006  meaiuninclem  41015  meaiininclem  41021  omeiunltfirp  41054  carageniuncllem1  41056  carageniuncllem2  41057  caratheodorylem1  41061  0ome  41064  vonval  41075  ovnval  41076  ovnval2  41080  hoicvr  41083  ovnval2b  41087  hoiprodcl2  41090  ovnlecvr  41093  ovncvrrp  41099  ovn0lem  41100  ovnsubaddlem1  41105  hsphoif  41111  hoidmvval  41112  hsphoival  41114  hoidmv1le  41129  hoidmvlelem3  41132  ovnhoilem1  41136  ovnhoilem2  41137  hoidifhspval  41143  hspval  41144  ovncvr2  41146  hoidifhspval2  41150  hoidifhspval3  41154  hspmbllem2  41162  ovnsubadd2lem  41180  vonioolem2  41216  vonicclem2  41219  issmflem  41257  smfid  41282  fvmptrab  41631  fvmptrabdm  41632  iccpval  41676  fmtno  41766  prmdvdsfmtnof1  41824  upwlksfval  42041  sprval  42054  sprsymrelfv  42069  uspgrsprfv  42078  clintopval  42165  assintopval  42166  c0mgm  42234  c0mhm  42235  c0snmgmhm  42239  c0snmhm  42240  zrrnghm  42242  rngcvalALTV  42286  rngcval  42287  rngcidALTV  42316  zrinitorngc  42325  zrtermorngc  42326  ringcvalALTV  42332  ringcval  42333  funcringcsetcALTV2lem1  42361  ringcidALTV  42379  funcringcsetclem1ALTV  42384  zrtermoringc  42395  rhmsubcALTVlem3  42431  scmsuppss  42478  ply1mulgsum  42503  lincop  42522  lincext3  42570  lindslinindsimp1  42571  lindsrng01  42582  lincresunit2  42592  lincresunit3lem1  42593  islindeps2  42597  fdivmptfv  42664  refdivmptfv  42665  bigoval  42668  blenval  42690  digfval  42716  amgmwlem  42876
  Copyright terms: Public domain W3C validator