Theorem fmptd 6385

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.)

Hypotheses

Ref	Expression
fmptd.1	|- ( ( ph /\ x e. A ) -> B e. C )
fmptd.2	|- F = ( x e. A |-> B )

Assertion

Ref	Expression
fmptd	|- ( ph -> F : A --> C )

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

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

Proof of Theorem fmptd

Step	Hyp	Ref	Expression
1		fmptd.1	. . 3 |- ( ( ph /\ x e. A ) -> B e. C )
2	1	ralrimiva 2966	. 2 |- ( ph -> A. x e. A B e. C )
3		fmptd.2	. . 3 |- F = ( x e. A |-> B )
4	3	fmpt 6381	. 2 |- ( A. x e. A B e. C <-> F : A --> C )
5	2, 4	sylib 208	1 |- ( ph -> F : A --> C )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   |-> cmpt 4729   -->wf 5884

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-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  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-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896

This theorem is referenced by:  fmpt3d  6386  fliftrel  6558  off  6912  caofinvl  6924  curry1f  7271  curry2f  7273  fnwelem  7292  fdiagfn  7901  resixpfo  7946  pw2f1olem  8064  mapxpen  8126  xpmapenlem  8127  unxpdomlem3  8166  fsuppmptdm  8286  fsuppmptif  8305  wdom2d  8485  cantnfp1lem1  8575  cantnfp1lem2  8576  cantnfp1lem3  8577  cantnflem1d  8585  cantnflem1  8586  cantnf  8590  fseqenlem1  8847  fseqenlem2  8848  dfac8clem  8855  ac5num  8859  acni2  8869  infpwfien  8885  coftr  9095  fin23lem39  9172  isf34lem2  9195  fin1a2lem12  9233  axcc2lem  9258  axdc2lem  9270  axdc3lem4  9275  pwcfsdom  9405  canthp1lem2  9475  wuncval2  9569  gruf  9633  rpnnen1lem1  11815  rpnnen1lem1OLD  11821  monoord2  12832  seqf1o  12842  ccatcl  13359  swrdcl  13419  revcl  13510  revlen  13511  ello1mpt  14252  lo1o12  14264  lo1eq  14299  rlimeq  14300  climmpt2  14304  climrecl  14314  climge0  14315  o1compt  14318  rlimcn1b  14320  rlimdiv  14376  isercoll2  14399  caurcvg2  14408  caucvg  14409  sumrblem  14442  summolem2a  14446  fsumf1o  14454  sumss  14455  fsumss  14456  fsumcl2lem  14462  fsumadd  14470  isumclim3  14490  isummulc2  14493  fsummulc2  14516  fsumrelem  14539  climfsum  14552  isumshft  14571  divcnv  14585  supcvg  14588  prodfdiv  14628  prodrblem  14659  prodmolem2a  14664  fprodf1o  14676  prodss  14677  fprodss  14678  fprodser  14679  fprodcl2lem  14680  fprodmul  14690  fproddiv  14691  fprodn0  14709  iprodclim3  14731  fprodefsum  14825  rpnnen2lem2  14944  crth  15483  eulerthlem1  15486  iserodd  15540  prmreclem2  15621  prmreclem6  15625  1arithlem3  15629  4sqlem11  15659  vdwapf  15676  vdwlem2  15686  vdwlem4  15688  vdwlem6  15690  vdwlem10  15694  ramub1lem2  15731  ramcl  15733  prmodvdslcmf  15751  prmgaplcm  15764  prdsplusg  16118  prdsmulr  16119  prdsvsca  16120  mrcflem  16266  mreacs  16319  acsfn  16320  homaf  16680  funcestrcsetclem3  16782  funcsetcestrclem3  16796  prfcl  16843  curf1cl  16868  hofcllem  16898  hofcl  16899  yonedalem3a  16914  yonedalem4c  16917  yonedainv  16921  prdspjmhm  17367  pwsco1mhm  17370  pwsco2mhm  17371  gsumz  17374  gsumwspan  17383  vrmdfval  17393  vrmdf  17395  frmdup1  17401  grpinvf  17466  cycsubgcl  17620  cycsubgss  17621  conjghm  17691  conjnmz  17694  qusghm  17697  galactghm  17823  symgextf  17837  symgfixf  17856  pmtrf  17875  pmtrdifwrdellem1  17901  psgnunilem5  17914  odf1  17979  dfod2  17981  odf1o2  17988  pgpssslw  18029  sylow2blem1  18035  pj1f  18110  frgpmhm  18178  vrgpf  18181  mulgmhm  18233  mulgghm  18234  iscyggen2  18283  cyggenod  18286  iscyg3  18288  gsummptfsadd  18324  gsumzsplit  18327  gsumsplit2  18329  gsummptfidmsplitres  18331  gsumconst  18334  gsummptshft  18336  gsummhm2  18339  gsummptmhm  18340  gsummptfidminv  18347  gsummptfssub  18349  gsumzunsnd  18355  gsummptf1o  18362  gsummpt1n0  18364  gsum2dlem1  18369  gsum2dlem2  18370  gsum2d  18371  prdsgsum  18377  dprdfeq0  18421  dprdlub  18425  dprdz  18429  dprd2dlem1  18440  dprd2da  18441  ablfac1b  18469  ablfac2  18488  srglmhm  18535  srgrmhm  18536  ringlghm  18604  ringrghm  18605  gsumdixp  18609  abvtrivd  18840  issrngd  18861  lmodvsghm  18924  lspf  18974  pwssplit0  19058  asclf  19337  snifpsrbag  19366  psrass1lem  19377  psrmulcllem  19387  psr1cl  19402  psrlidm  19403  psrridm  19404  psrcom  19409  resspsrmul  19417  subrgpsr  19419  mvrf  19424  mplmon  19463  mplmonmul  19464  mplcoe1  19465  mplcoe5lem  19467  mplcoe5  19468  mplbas2  19470  psrbagsn  19495  evlslem4  19508  evlslem2  19512  evlslem6  19513  evlslem3  19514  evlslem1  19515  evlsval2  19520  psropprmul  19608  coe1mul2  19639  coe1tmmul2  19646  coe1tmmul  19647  ply1coe  19666  gsumsmonply1  19673  gsummoncoe1  19674  gsumfsum  19813  regsumfsum  19814  expmhm  19815  expghm  19844  mulgghm2  19845  evpmodpmf1o  19942  isphld  19999  pjff  20056  frlmgsum  20111  frlmsplit2  20112  frlmphl  20120  uvcff  20130  uvcresum  20132  frlmup1  20137  mamulid  20247  mamurid  20248  scmatf  20335  mdetf  20401  mdetunilem9  20426  mdetuni0  20427  mdetmul  20429  maduf  20447  smadiadetlem3lem1  20472  cpm2mf  20557  m2cpmfo  20561  pmatcollpw1  20581  pmatcollpw3lem  20588  pmatcollpw3fi1lem1  20591  pmatcollpw3fi1lem2  20592  pm2mpcl  20602  mply1topmatcl  20610  mp2pm2mplem2  20612  mp2pm2mp  20616  pm2mpmhmlem2  20624  chfacfisf  20659  chfacfisfcpmat  20660  cpmidpmatlem2  20676  cayhamlem4  20693  pptbas  20812  tgrest  20963  resttopon  20965  rest0  20973  restfpw  20983  ordtbaslem  20992  ordtuni  20994  ordtrest  21006  cnpfval  21038  pnrmopn  21147  cncmp  21195  discmp  21201  1stcfb  21248  2ndcomap  21261  dis2ndc  21263  lly1stc  21299  comppfsc  21335  kgencmp  21348  ptpjpre1  21374  ptpjcn  21414  ptcldmpt  21417  ptclsg  21418  dfac14  21421  xkoccn  21422  txcnp  21423  ptcnp  21425  txcnmpt  21427  uptx  21428  ptcn  21430  ptrescn  21442  txlm  21451  xkoptsub  21457  xkoco1cn  21460  xkoco2cn  21461  cnmpt11  21466  xkoinjcn  21490  kqffn  21528  pt1hmeo  21609  fbasrn  21688  trfilss  21693  trfg  21695  rnelfmlem  21756  txflf  21810  flfcnp2  21811  fclscmpi  21833  alexsublem  21848  ptcmplem3  21858  symgtgp  21905  subgntr  21910  opnsubg  21911  clsnsg  21913  tgpconncomp  21916  tsmsfbas  21931  eltsms  21936  haustsms  21939  tsmscls  21941  tsms0  21945  tsmsmhm  21949  tgptsmscls  21953  tsmssplit  21955  tsmsxplem1  21956  tsmsxplem2  21957  ustuqtop0  22044  prdsdsf  22172  prdsxmetlem  22173  imasdsf1olem  22178  prdsbl  22296  stdbdxmet  22320  met1stc  22326  nmf2  22397  xrge0gsumle  22636  xrge0tsms  22637  metdsf  22651  metdsge  22652  mulc1cncf  22708  cncfmpt2ss  22718  cnmptre  22726  evth  22758  evth2  22759  lebnumlem1  22760  cphnmf  22995  tchcph  23036  cmetcaulem  23086  rrxmval  23188  minveclem1  23195  minveclem3b  23199  ovollb2lem  23256  ovolctb  23258  ovolunlem1a  23264  ovolunlem1  23265  ovoliunlem1  23270  ovoliunlem2  23271  ovoliun  23273  ovolshftlem1  23277  ovolscalem1  23281  ovolicc1  23284  iunmbl  23321  ioombl1lem1  23326  uniioombllem2  23351  uniioombllem3  23353  volsup2  23373  volcn  23374  vitalilem4  23380  vitalilem5  23381  mbfconst  23402  ismbfcn2  23406  mbfeqalem  23409  mbfss  23413  mbfmulc2re  23415  mbfmax  23416  mbfneg  23417  mbfpos  23418  mbfposr  23419  mbfposb  23420  mbfadd  23428  mbfmulc2  23430  mbfsup  23431  mbfinf  23432  mbflimsup  23433  mbflimlem  23434  mbflim  23435  i1f1lem  23456  i1f1  23457  i1fres  23472  itg1climres  23481  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  mbfi1flimlem  23489  mbfi1flim  23490  mbfmullem2  23491  mbfmul  23493  itg2const2  23508  itg2seq  23509  itg2splitlem  23515  itg2split  23516  itg2monolem1  23517  itg2monolem2  23518  itg2monolem3  23519  itg2mono  23520  itg2i1fseq  23522  itg2i1fseq2  23523  itg2gt0  23527  itg2cnlem1  23528  itg2cnlem2  23529  itg2cn  23530  iblss  23571  itgitg1  23575  itgle  23576  itgeqa  23580  itgss3  23581  ibladdlem  23586  itgaddlem1  23589  iblabslem  23594  iblabs  23595  iblabsr  23596  iblmulc2  23597  itgmulc2lem1  23598  bddmulibl  23605  itggt0  23608  itgcn  23609  ellimc2  23641  limcmpt  23647  limcres  23650  limccnp  23655  limccnp2  23656  limcco  23657  perfdvf  23667  dvreslem  23673  dvcnp2  23683  dvaddbr  23701  dvmulbr  23702  dvcjbr  23712  dvexp  23716  dvrec  23718  dvmptres3  23719  dvmptadd  23723  dvmptmul  23724  dvmptres2  23725  dvmptcmul  23727  dvmptcj  23731  dvmptntr  23734  dvmptco  23735  dvcnvlem  23739  dvef  23743  dvferm1  23748  dvferm2  23750  rolle  23753  dvlipcn  23757  dvle  23770  dvivthlem1  23771  dvivth  23773  lhop1lem  23776  lhop1  23777  lhop2  23778  lhop  23779  dvfsumle  23784  dvfsumge  23785  dvmptrecl  23787  dvfsumrlimf  23788  dvfsumlem2  23790  dvfsumlem3  23791  ftc1lem2  23799  ftc1lem6  23804  itgsubstlem  23811  tdeglem1  23818  tdeglem4  23820  coe1mul3  23859  elply2  23952  plyf  23954  elplyd  23958  plypf1  23968  coeeq2  23998  coemullem  24006  coe1termlem  24014  dvply2g  24040  elqaalem2  24075  taylfvallem  24112  taylf  24115  tayl0  24116  taylpfval  24119  taylpf  24120  taylthlem1  24127  taylthlem2  24128  ulmshftlem  24143  ulmshft  24144  ulmcau  24149  ulmss  24151  ulmdvlem1  24154  ulmdvlem3  24156  mtest  24158  mtestbdd  24159  itgulm2  24163  psergf  24166  radcnvlem1  24167  dvradcnv  24175  pserulm  24176  psercn2  24177  pserdvlem2  24182  abelthlem4  24188  abelthlem9  24194  pige3  24269  efif1olem4  24291  logtayl  24406  logccv  24409  loglesqrt  24499  logbf  24527  leibpi  24669  rlimcnp  24692  rlimcnp2  24693  xrlimcnp  24695  efrlim  24696  dfef2  24697  o1cxp  24701  cxp2lim  24703  amgmlem  24716  lgamgulmlem2  24756  lgamgulmlem6  24760  lgamcvg2  24781  gamcvg  24782  regamcl  24787  relgamcl  24788  basellem2  24808  basellem4  24810  basellem7  24813  basellem9  24815  sqff1o  24908  fsumvma  24938  dchrelbasd  24964  lgsfcl2  25028  lgsqrlem2  25072  lgseisenlem1  25100  lgseisenlem3  25102  lgseisenlem4  25103  chpo1ub  25169  dchrmusum2  25183  dchrvmasumiflem1  25190  dchrisum0ff  25196  dchrisum0lem1b  25204  dchrisum0lem2a  25206  logsqvma2  25232  pnt2  25302  pnt  25303  abvcxp  25304  padicabv  25319  lmif  25677  axlowdimlem15  25836  incistruhgr  25974  vtxdgf  26367  crctcshwlkn0  26713  wlkiswwlks2lem5  26759  wlkpwwlkf1ouspgr  26765  wlknwwlksnfun  26774  wlkwwlkfun  26781  wwlksnextfun  26793  clwlkclwwlklem2a  26899  clwwlksf  26915  clwlksfclwwlk  26962  frgrncvvdeqlem4  27166  numclwlk1lem2f  27225  numclwlk2lem2f  27236  ipblnfi  27711  ubthlem1  27726  minvecolem1  27730  htthlem  27774  hlimadd  28050  chscllem1  28496  hoaddcl  28617  homulcl  28618  brafn  28806  kbop  28812  cnlnadjlem2  28927  strlem3a  29111  hstrlem3a  29119  off2  29443  xppreima2  29450  fpwrelmap  29508  gsummpt2d  29781  gsumvsca1  29782  gsumvsca2  29783  xrge0tsmsd  29785  ordtrestNEW  29967  xrge0mulc1cn  29987  esumf1o  30112  esumadd  30119  esumcst  30125  esumpfinval  30137  esumpcvgval  30140  esumcvg  30148  esumsup  30151  measinb  30284  measdivcst  30288  mbfmco2  30327  sitgclg  30404  eulerpartlems  30422  dstfrvclim1  30539  gsumncl  30614  gsumnunsn  30615  fdvneggt  30678  fdvnegge  30680  itgexpif  30684  logdivsqrle  30728  erdszelem9  31181  indispconn  31216  cvxpconn  31224  cvmsss2  31256  cvmliftlem6  31272  cvmliftlem8  31274  cvmlift3lem3  31303  mrsubcv  31407  mrsubff  31409  mrsubrn  31410  mrsubccat  31415  elmrsubrn  31417  msubrn  31426  msubff  31427  mvhf  31455  divcnvlin  31618  iprodefisum  31627  faclimlem2  31630  faclim  31632  faclim2  31634  knoppcnlem5  32487  knoppcnlem8  32490  knoppcnlem10  32492  knoppcnlem11  32493  unbdqndv1  32499  knoppf  32526  curf  33387  finixpnum  33394  matunitlindflem1  33405  matunitlindflem2  33406  ptrest  33408  poimirlem17  33426  poimirlem20  33429  poimirlem24  33433  poimirlem30  33439  broucube  33443  mblfinlem2  33447  volsupnfl  33454  mbfposadd  33457  itg2addnclem2  33462  itg2gt0cn  33465  ibladdnclem  33466  itgaddnclem1  33468  itgaddnc  33470  iblabsnclem  33473  iblabsnc  33474  iblmulc2nc  33475  itgmulc2nclem1  33476  itgmulc2nclem2  33477  itgmulc2nc  33478  itgabsnc  33479  bddiblnc  33480  itggt0cn  33482  ftc1cnnc  33484  ftc1anclem1  33485  ftc1anclem2  33486  ftc1anclem3  33487  ftc1anclem4  33488  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  areacirclem4  33503  upixp  33524  totbndbnd  33588  prdsbnd  33592  cntotbnd  33595  rrnequiv  33634  lsatlss  34283  lflnegcl  34362  lshpkrcl  34403  tendoplcl  36069  tendo0cl  36078  tendoicl  36084  cmpfiiin  37260  mzpclall  37290  mzpindd  37309  fphpdo  37381  dnnumch3  37617  kelac1  37633  dfac21  37636  itgpowd  37800  rfovcnvf1od  38298  fsovfd  38306  fsovcnvlem  38307  clsk3nimkb  38338  expgrowth  38534  binomcxplemradcnv  38551  binomcxplemcvg  38553  binomcxplemnotnn0  38555  rnmptc  39353  mptelpm  39357  projf1o  39386  mapss2  39397  expcnfg  39823  clim1fr1  39833  mullimc  39848  ellimcabssub0  39849  mullimcf  39855  constlimc  39856  idlimc  39858  sumnnodd  39862  neglimc  39879  addlimc  39880  0ellimcdiv  39881  fnlimf  39910  limsupvaluz2  39970  supcnvlimsup  39972  climliminflimsupd  40033  cncfmptssg  40083  cncfshift  40087  cncfcompt  40096  icccncfext  40100  cncfiooiccre  40108  cxpcncf2  40113  fprodsubrecnncnvlem  40121  fprodaddrecnncnvlem  40123  dvsinax  40127  fperdvper  40133  dvmptresicc  40134  dvcosax  40141  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnmptdivc  40153  dvnxpaek  40157  dvnprodlem1  40161  dvnprodlem2  40162  dvnprodlem3  40163  itgsinexplem1  40169  iblsplit  40182  itgcoscmulx  40185  itgiccshift  40196  itgperiod  40197  itgsbtaddcnst  40198  dirkerf  40314  dirkeritg  40319  dirkercncflem2  40321  fourierdlem4  40328  fourierdlem5  40329  fourierdlem9  40333  fourierdlem14  40338  fourierdlem16  40340  fourierdlem17  40341  fourierdlem18  40342  fourierdlem21  40345  fourierdlem22  40346  fourierdlem37  40361  fourierdlem50  40373  fourierdlem51  40374  fourierdlem53  40376  fourierdlem55  40378  fourierdlem57  40380  fourierdlem58  40381  fourierdlem59  40382  fourierdlem60  40383  fourierdlem61  40384  fourierdlem67  40390  fourierdlem68  40391  fourierdlem72  40395  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem78  40401  fourierdlem80  40403  fourierdlem81  40404  fourierdlem83  40406  fourierdlem84  40407  fourierdlem88  40411  fourierdlem92  40415  fourierdlem93  40416  fourierdlem97  40420  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  sqwvfoura  40445  elaa2lem  40450  etransclem1  40452  etransclem8  40459  etransclem20  40471  etransclem33  40484  etransclem35  40486  etransclem39  40490  rrxtopnfi  40506  ioorrnopnxrlem  40526  sge0tsms  40597  sge0snmpt  40600  sge0fsummpt  40607  sge0pr  40611  sge0lessmpt  40616  sge0iunmptlemfi  40630  sge0iunmptlemre  40632  sge0iunmpt  40635  sge0rpcpnf  40638  sge0isum  40644  nnfoctbdjlem  40672  psmeasure  40688  voliunsge0lem  40689  meaiuninclem  40697  meaiininclem  40700  omeiunltfirp  40733  carageniuncllem2  40736  caratheodorylem1  40740  caratheodorylem2  40741  isomenndlem  40744  hoicvr  40762  hoicvrrex  40770  ovnsupge0  40771  ovnlecvr  40772  ovnf  40777  ovn0lem  40779  ovnsubaddlem1  40784  ovnsubadd  40786  hsphoif  40790  sge0hsphoire  40803  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmv1lelem3  40807  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem5  40813  ovnhoilem1  40815  ovnhoilem2  40816  ovnlecvr2  40824  ovncvr2  40825  hoidifhspf  40832  hspmbllem2  40841  opnvonmbllem2  40847  ovnsubadd2lem  40859  ovolval4lem1  40863  ovolval4lem2  40864  ovolval5lem2  40867  ovnovollem1  40870  ovnovollem2  40871  iccvonmbllem  40892  vonioolem1  40894  vonioolem2  40895  vonicclem1  40897  vonicclem2  40898  smfid  40961  smfmbfcex  40968  smflim  40985  nsssmfmbflem  40986  smfmullem4  41001  smfsuplem1  41017  smfsuplem3  41019  smflimsuplem3  41028  pfxf  41389  fmtnodvds  41456  c0mgm  41909  c0mhm  41910  c0snmgmhm  41914  funcringcsetcALTV2lem3  42038  funcringcsetclem3ALTV  42061  gsumlsscl  42164  ply1mulgsum  42178  lincfsuppcl  42202  linccl  42203  lincvalsc0  42210  lcoc0  42211  linc0scn0  42212  linc1  42214  lincsum  42218  lincscm  42219  lincscmcl  42221  lcoss  42225  lincext1  42243  el0ldep  42255  lincresunit1  42266  lincresunit3  42270  lmod1zr  42282  fdivmptf  42335  refdivmptf  42336  aacllem  42547  amgmwlem  42548  amgmlemALT  42549