Theorem fvmptd 6288

Description: Deduction version of fvmpt 6282. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)

Hypotheses

Ref	Expression
fvmptd.1	|- ( ph -> F = ( x e. D |-> B ) )
fvmptd.2	|- ( ( ph /\ x = A ) -> B = C )
fvmptd.3	|- ( ph -> A e. D )
fvmptd.4	|- ( ph -> C e. V )

Assertion

Ref	Expression
fvmptd	|- ( ph -> ( F ` A ) = C )

Distinct variable groups:   x, A   x, C   x, D   ph, x

Allowed substitution hints:   B( x)   F( x)   V( x)

Proof of Theorem fvmptd

Step	Hyp	Ref	Expression
1		fvmptd.1	. . 3 |- ( ph -> F = ( x e. D |-> B ) )
2	1	fveq1d 6193	. 2 |- ( ph -> ( F ` A ) = ( ( x e. D |-> B ) ` A ) )
3		fvmptd.3	. . 3 |- ( ph -> A e. D )
4		fvmptd.2	. . . . 5 |- ( ( ph /\ x = A ) -> B = C )
5	3, 4	csbied 3560	. . . 4 |- ( ph -> [_ A / x ]_ B = C )
6		fvmptd.4	. . . 4 |- ( ph -> C e. V )
7	5, 6	eqeltrd 2701	. . 3 |- ( ph -> [_ A / x ]_ B e. V )
8		eqid 2622	. . . 4 |- ( x e. D |-> B ) = ( x e. D |-> B )
9	8	fvmpts 6285	. . 3 |- ( ( A e. D /\ [_ A / x ]_ B e. V ) -> ( ( x e. D |-> B ) ` A ) = [_ A / x ]_ B )
10	3, 7, 9	syl2anc 693	. 2 |- ( ph -> ( ( x e. D |-> B ) ` A ) = [_ A / x ]_ B )
11	2, 10, 5	3eqtrd 2660	1 |- ( ph -> ( F ` A ) = C )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   [_csb 3533   |-> cmpt 4729   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896

This theorem is referenced by:  fvmptdv2  6298  fvmptopab  6697  mptmpt2opabbrd  7248  bropfvvvv  7257  mpt2curryvald  7396  ttukeylem3  9333  ccatval1  13361  ccatval2  13362  repswsymb  13521  relexp1g  13766  rtrclreclem2  13799  rtrclreclem4  13801  dfrtrcl2  13802  lcmfval  15334  lcmf0val  15335  prmoval  15737  fvprmselelfz  15748  fvprmselgcd1  15749  prmodvdslcmf  15751  prmgap  15763  prmgaplcm  15764  prmgapprmo  15766  prdsvscafval  16140  mrcval  16270  cidval  16338  isofval  16417  isofn  16435  cicfval  16457  subcid  16507  idfu2nd  16537  resf2nd  16555  fuccoval  16623  fucid  16631  initoval  16647  termoval  16648  zerooval  16649  homaval  16681  idaval  16708  setcval  16727  setcid  16736  catcval  16746  catcid  16753  estrcval  16764  estrcid  16774  funcestrcsetclem1  16780  funcsetcestrclem1  16794  prf1  16840  prf2  16842  curf1  16865  curf11  16866  curf2val  16870  hofval  16892  hof2  16897  yonval  16901  yonedalem4a  16915  frmdval  17388  vrmdval  17394  pmtrdifwrdellem3  17903  gexval  17993  pj1val  18108  dpjval  18455  sraval  19176  opsrval  19474  cply1mul  19664  cply1coe0  19669  cply1coe0bi  19670  gsummoncoe1  19674  evls1sca  19688  frlmphl  20120  mat1rhmval  20285  scmatrhmval  20333  mvmulfv  20350  mavmulfv  20352  mdetuni0  20427  mat2pmatval  20529  m2cpm  20546  cpm2mval  20555  m2cpminvid2lem  20559  decpmatid  20575  decpmatmullem  20576  pmatcollpw2lem  20582  monmatcollpw  20584  pmatcollpw3fi1lem1  20591  pm2mpfval  20601  mply1topmatval  20609  mp2pm2mplem1  20611  mp2pm2mplem4  20614  pm2mpmhmlem2  20624  chpmatval  20636  chfacfscmul0  20663  chfacfscmulgsum  20665  chfacfpmmul0  20667  chfacfpmmulgsum  20669  lmfval  21036  kgenval  21338  ptval  21373  fcfval  21837  cnextfval  21866  ustval  22006  utopval  22036  ustuqtoplem  22043  utopsnneiplem  22051  tusval  22070  blfvalps  22188  tmsval  22286  metuval  22354  caufval  23073  rrxmvallem  23187  rrxmval  23188  taylpval  24121  efgh  24287  lgamgulmlem2  24756  lgamcvglem  24766  logexprlim  24950  dchrval  24959  dchr1  24982  gausslemma2dlem2  25092  gausslemma2dlem3  25093  gausslemma2dlem4  25094  2lgslem1b  25117  ishlg  25497  mirval  25550  mirfv  25551  israg  25592  perpln1  25605  perpln2  25606  isperp  25607  ishpg  25651  midf  25668  ismidb  25670  lmif  25677  islmib  25679  edgval  25941  edgvalOLD  25942  uvtxaval  26287  vtxdgfval  26363  wksfval  26505  crctcshwlkn0lem2  26703  crctcshwlkn0lem3  26704  crctcsh  26716  wwlks  26727  wlkiswwlks2lem2  26756  wlkpwwlkf1ouspgr  26765  clwwlks  26879  clwlkclwwlklem2fv1  26896  clwlkclwwlklem2fv2  26897  numclwlk2lem2fv  27237  sgnsval  29728  psgnfzto1stlem  29850  fzto1stfv1  29851  madjusmdetlem2  29894  metidval  29933  pstmval  29938  qqhvval  30027  indv  30074  indval  30075  indfval  30078  esummulc1  30143  esumcvg  30148  ofcval  30161  sigagenval  30203  measinb  30284  omsval  30355  omsfval  30356  omssubadd  30362  carsgval  30365  sitgfval  30403  eulerpartlemsv1  30418  eulerpartlems  30422  eulerpartlemgvv  30438  fibp1  30463  totprobd  30488  probmeasb  30492  cndprobval  30495  dstrvprob  30533  dstfrvinc  30538  dstfrvclim1  30539  ballotlemfval  30551  ballotlemsv  30571  gsumnunsn  30615  signsply0  30628  signstfval  30641  fdvneggt  30678  fdvnegge  30680  itgexpif  30684  reprval  30688  breprexplema  30708  vtsval  30715  logdivsqrle  30728  hgt750lemg  30732  hgt750lemb  30734  afsval  30749  cvmliftlem9  31275  mvrsval  31402  mrsubfval  31405  mrsubval  31406  msubfval  31421  msubval  31422  msrval  31435  fwddifval  32269  fwddifnval  32270  knoppcnlem1  32483  knoppcnlem4  32486  knoppcnlem6  32488  knoppcnlem7  32489  knoppcnlem9  32491  unbdqndv2lem2  32501  knoppndvlem4  32506  knoppndvlem6  32508  bj-finsumval0  33147  poimirlem1  33410  poimirlem2  33411  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem19  33428  poimirlem22  33431  mblfinlem2  33447  areacirc  33505  cdleme31fv2  35681  tendopl2  36065  tendoi2  36083  erngplus2  36092  erngplus2-rN  36100  hlhilset  37226  itgpowd  37800  iunrelexpmin1  38000  iunrelexpmin2  38004  rfovfvd  38296  rfovfvfvd  38297  rfovcnvf1od  38298  rfovcnvfvd  38301  fsovfvd  38304  fsovfvfvd  38305  fsovcnvlem  38307  dssmapfvd  38311  dssmapfv2d  38312  dssmapfv3d  38313  dssmapnvod  38314  clsk3nimkb  38338  dvgrat  38511  radcnvrat  38513  hashnzfzclim  38521  binomcxplemnn0  38548  binomcxplemrat  38549  binomcxplemfrat  38550  binomcxplemradcnv  38551  binomcxplemcvg  38553  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  projf1o  39386  mapss2  39397  fvmptd2  39445  fmuldfeqlem1  39814  clim1fr1  39833  climrec  39835  climexp  39837  climneg  39842  mullimcf  39855  divcnvg  39859  sumnnodd  39862  expfac  39889  fnlimfv  39895  fnlimabslt  39911  supcnvlimsup  39972  cncfshift  40087  icccncfext  40100  cncfioobdlem  40109  fprodsubrecnncnvlem  40121  fprodaddrecnncnvlem  40123  dvsinax  40127  fperdvper  40133  dvcosax  40141  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnmul  40158  dvnprodlem1  40161  dvnprodlem2  40162  dvnprodlem3  40163  itgsinexp  40170  itgcoscmulx  40185  itgsincmulx  40190  itgsubsticclem  40191  itgsubsticc  40192  itgiccshift  40196  stoweidlem7  40224  stoweidlem17  40234  stoweidlem32  40249  stoweidlem34  40251  wallispilem4  40285  wallispilem5  40286  wallispi  40287  wallispi2lem1  40288  wallispi2lem2  40289  wallispi2  40290  stirlinglem1  40291  stirlinglem2  40292  stirlinglem3  40293  stirlinglem4  40294  stirlinglem5  40295  stirlinglem7  40297  stirlinglem8  40298  stirlinglem10  40300  stirlinglem11  40301  stirlinglem12  40302  stirlinglem13  40303  stirlinglem14  40304  stirlinglem15  40305  dirkerval2  40311  dirkercncflem2  40321  fourierdlem7  40331  fourierdlem13  40337  fourierdlem14  40338  fourierdlem16  40340  fourierdlem18  40342  fourierdlem19  40343  fourierdlem21  40345  fourierdlem22  40346  fourierdlem26  40350  fourierdlem37  40361  fourierdlem39  40363  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem51  40374  fourierdlem53  40376  fourierdlem62  40385  fourierdlem63  40386  fourierdlem65  40388  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem79  40402  fourierdlem81  40404  fourierdlem82  40405  fourierdlem83  40406  fourierdlem84  40407  fourierdlem88  40411  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem92  40415  fourierdlem93  40416  fourierdlem97  40420  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem112  40435  fouriersw  40448  elaa2lem  40450  etransclem1  40452  etransclem12  40463  etransclem13  40464  etransclem17  40468  etransclem18  40469  etransclem21  40472  etransclem27  40478  etransclem31  40482  etransclem32  40483  etransclem33  40484  etransclem35  40486  etransclem46  40497  etransclem48  40499  rrxtopnfi  40506  salgenval  40541  sge0val  40583  sge0z  40592  sge0snmpt  40600  sge0xp  40646  nnfoctbdjlem  40672  psmeasurelem  40687  psmeasure  40688  meaiuninclem  40697  meaiininclem  40700  omeiunltfirp  40733  carageniuncllem1  40735  carageniuncllem2  40736  caratheodorylem1  40740  0ome  40743  vonval  40754  ovnval  40755  ovnval2  40759  hoicvr  40762  ovnval2b  40766  hoiprodcl2  40769  ovnlecvr  40772  ovncvrrp  40778  ovn0lem  40779  ovnsubaddlem1  40784  hsphoif  40790  hoidmvval  40791  hsphoival  40793  hoidmv1le  40808  hoidmvlelem3  40811  ovnhoilem1  40815  ovnhoilem2  40816  hoidifhspval  40822  hspval  40823  ovncvr2  40825  hoidifhspval2  40829  hoidifhspval3  40833  hspmbllem2  40841  ovnsubadd2lem  40859  vonioolem2  40895  vonicclem2  40898  issmflem  40936  smfid  40961  iccpval  41351  fmtno  41441  prmdvdsfmtnof1  41499  upwlksfval  41716  sprval  41729  sprsymrelfv  41744  uspgrsprfv  41753  clintopval  41840  assintopval  41841  c0mgm  41909  c0mhm  41910  c0snmgmhm  41914  c0snmhm  41915  zrrnghm  41917  rngcvalALTV  41961  rngcval  41962  rngcidALTV  41991  zrinitorngc  42000  zrtermorngc  42001  ringcvalALTV  42007  ringcval  42008  funcringcsetcALTV2lem1  42036  ringcidALTV  42054  funcringcsetclem1ALTV  42059  zrtermoringc  42070  rhmsubcALTVlem3  42106  scmsuppss  42153  ply1mulgsum  42178  lincop  42197  lincext3  42245  lindslinindsimp1  42246  lindsrng01  42257  lincresunit2  42267  lincresunit3lem1  42268  islindeps2  42272  fdivmptfv  42339  refdivmptfv  42340  bigoval  42343  blenval  42365  digfval  42391  amgmwlem  42548