MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fmptd Structured version   Unicode version

Theorem fmptd 6059
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
StepHypRef Expression
1 fmptd.1 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  C )
21ralrimiva 2840 . 2  |-  ( ph  ->  A. x  e.  A  B  e.  C )
3 fmptd.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43fmpt 6056 . 2  |-  ( A. x  e.  A  B  e.  C  <->  F : A --> C )
52, 4sylib 200 1  |-  ( ph  ->  F : A --> C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1438    e. wcel 1869   A.wral 2776    |-> cmpt 4480   -->wf 5595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-sbc 3301  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-opab 4481  df-mpt 4482  df-id 4766  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-fv 5607
This theorem is referenced by:  fmpt3d  6060  fmptco  6069  fliftrel  6214  off  6558  caofinvl  6570  curry1f  6899  curry2f  6901  fnwelem  6920  fdiagfn  7521  resixpfo  7566  pw2f1olem  7680  mapxpen  7742  xpmapenlem  7743  unxpdomlem3  7782  fsuppmptdm  7898  fsuppmptif  7917  wdom2d  8099  cantnfp1lem1  8186  cantnfp1lem2  8187  cantnfp1lem3  8188  cantnflem1d  8196  cantnflem1  8197  cantnf  8201  fseqenlem1  8457  fseqenlem2  8458  dfac8clem  8465  ac5num  8469  acni2  8479  infpwfien  8495  coftr  8705  fin23lem39  8782  isf34lem2  8805  fin1a2lem12  8843  axcc2lem  8868  axdc2lem  8880  axdc3lem4  8885  pwcfsdom  9010  canthp1lem2  9080  wuncval2  9174  gruf  9238  rpnnen1lem1  11292  monoord2  12245  seqf1o  12255  ccatcl  12718  swrdcl  12771  revcl  12862  revlen  12863  ello1mpt  13578  lo1o12  13590  lo1eq  13625  rlimeq  13626  climmpt2  13630  climrecl  13640  climge0  13641  o1compt  13644  rlimcn1b  13646  rlimdiv  13702  isercoll2  13725  caurcvg2  13737  caucvg  13738  sumrblem  13770  summolem2a  13774  fsumf1o  13782  sumss  13783  fsumss  13784  fsumcl2lem  13790  fsumadd  13798  isumclim3  13813  isummulc2  13816  fsummulc2  13838  fsumrelem  13860  climfsum  13873  isumshft  13890  divcnv  13904  supcvg  13907  prodfdiv  13945  prodrblem  13976  prodmolem2a  13981  fprodf1o  13993  prodss  13994  fprodss  13995  fprodser  13996  fprodcl2lem  13997  fprodmul  14007  fproddiv  14008  fprodn0  14026  iprodclim3  14046  fprodefsum  14142  rpnnen2lem2  14261  crt  14719  eulerthlem1  14722  iserodd  14778  prmreclem2  14854  prmreclem6  14858  1arithlem3  14862  4sqlem11  14892  vdwapf  14915  vdwlem2  14925  vdwlem4  14927  vdwlem6  14929  vdwlem10  14933  ramub1lem2  14978  ramcl  14980  prmodvdslcmf  14998  prmordvdslcmfOLD  15012  prmordvdslcmsOLDOLD  15014  prmgaplcm  15024  prdsplusg  15349  prdsmulr  15350  prdsvsca  15351  mrcflem  15505  mreacs  15557  acsfn  15558  homaf  15918  funcestrcsetclem3  16020  funcsetcestrclem3  16034  prfcl  16081  curf1cl  16106  hofcllem  16136  hofcl  16137  yonedalem3a  16152  yonedalem4c  16155  yonedainv  16159  prdspjmhm  16607  pwsco1mhm  16610  pwsco2mhm  16611  gsumz  16614  gsumwspan  16623  vrmdfval  16633  vrmdf  16635  frmdup1  16641  grpinvf  16703  cycsubgcl  16836  cycsubgss  16837  conjghm  16906  conjnmz  16909  qusghm  16912  galactghm  17037  symgextf  17051  symgfixf  17070  pmtrf  17089  pmtrdifwrdellem1  17115  psgnunilem5  17128  odf1  17206  dfod2  17208  odf1o2  17215  pgpssslw  17259  sylow2blem1  17265  pj1f  17340  frgpmhm  17408  vrgpf  17411  mulgmhm  17461  mulgghm  17462  iscyggen2  17509  cyggenod  17512  iscyg3  17514  gsummptfsadd  17550  gsumzsplit  17553  gsumsplit2  17555  gsummptfidmsplitres  17557  gsumconst  17560  gsummptshft  17562  gsummhm2  17565  gsummptmhm  17566  gsummptfidminv  17573  gsummptfssub  17575  gsumzunsnd  17581  gsummptf1o  17588  gsummpt1n0  17590  gsum2dlem1  17595  gsum2dlem2  17596  gsum2d  17597  prdsgsum  17603  dprdfeq0  17648  dprdlub  17652  dprdz  17656  dprd2dlem1  17667  dprd2da  17668  ablfac1b  17696  ablfac2  17715  srglmhm  17761  srgrmhm  17762  ringlghm  17825  ringrghm  17826  gsumdixp  17830  abvtrivd  18061  issrngd  18082  lmodvsghm  18142  lspf  18190  pwssplit0  18274  asclf  18554  snifpsrbag  18583  psrass1lem  18594  psrmulcllem  18604  psr1cl  18619  psrlidm  18620  psrridm  18621  psrcom  18626  resspsrmul  18634  subrgpsr  18636  mvrf  18641  mplmon  18680  mplmonmul  18681  mplcoe1  18682  mplcoe5lem  18684  mplcoe5  18685  mplbas2  18687  psrbagsn  18711  evlslem4  18724  evlslem2  18728  evlslem6  18729  evlslem3  18730  evlslem1  18731  evlsval2  18736  psropprmul  18824  coe1mul2  18855  coe1tmmul2  18862  coe1tmmul  18863  ply1coe  18882  ply1coeOLD  18883  gsumsmonply1  18890  gsummoncoe1  18891  gsumfsum  19027  expmhm  19028  expghm  19059  mulgghm2  19060  evpmodpmf1o  19156  isphld  19213  pjff  19267  frlmgsum  19322  frlmsplit2  19323  frlmphl  19331  uvcff  19341  uvcresum  19343  frlmup1  19348  mamulid  19458  mamurid  19459  scmatf  19546  mdetf  19612  mdetunilem9  19637  mdetuni0  19638  mdetmul  19640  maduf  19658  smadiadetlem3lem1  19683  cpm2mf  19768  m2cpmfo  19772  pmatcollpw1  19792  pmatcollpw3lem  19799  pmatcollpw3fi1lem1  19802  pmatcollpw3fi1lem2  19803  pm2mpcl  19813  mply1topmatcl  19821  mp2pm2mplem2  19823  mp2pm2mp  19827  pm2mpmhmlem2  19835  chfacfisf  19870  chfacfisfcpmat  19871  cpmidpmatlem2  19887  cayhamlem4  19904  pptbas  20015  tgrest  20167  resttopon  20169  rest0  20177  restfpw  20187  ordtbaslem  20196  ordtuni  20198  ordtrest  20210  cnpfval  20242  pnrmopn  20351  cncmp  20399  discmp  20405  1stcfb  20452  2ndcomap  20465  dis2ndc  20467  lly1stc  20503  comppfsc  20539  kgencmp  20552  ptpjpre1  20578  ptpjcn  20618  ptcldmpt  20621  ptclsg  20622  dfac14  20625  xkoccn  20626  txcnp  20627  ptcnp  20629  txcnmpt  20631  uptx  20632  ptcn  20634  ptrescn  20646  txlm  20655  xkoptsub  20661  xkoco1cn  20664  xkoco2cn  20665  cnmpt11  20670  xkoinjcn  20694  kqffn  20732  pt1hmeo  20813  fbasrn  20891  trfilss  20896  trfg  20898  rnelfmlem  20959  txflf  21013  flfcnp2  21014  fclscmpi  21036  alexsublem  21051  ptcmplem3  21061  symgtgp  21108  subgntr  21113  opnsubg  21114  clsnsg  21116  tgpconcomp  21119  tsmsfbas  21134  eltsms  21139  haustsms  21142  tsmscls  21144  tsms0  21148  tsmsmhm  21152  tgptsmscls  21156  tsmssplit  21158  tsmsxplem1  21159  tsmsxplem2  21160  ustuqtop0  21247  prdsdsf  21374  prdsxmetlem  21375  imasdsf1olem  21380  prdsbl  21498  stdbdxmet  21522  met1stc  21528  nmf2  21599  nmofOLD  21734  xrge0gsumle  21843  xrge0tsms  21844  metdsf  21857  metdsge  21858  metdsfOLD  21872  metdsgeOLD  21873  mulc1cncf  21929  cncfmpt2ss  21939  cnmptre  21947  evth  21979  evth2  21980  lebnumlem1  21981  lebnumlem1OLD  21984  cphnmf  22165  tchcph  22203  cmetcaulem  22250  rrxmval  22351  minveclem1  22358  minveclem3b  22362  minveclem3bOLD  22374  ovollb2lem  22433  ovolctb  22435  ovolunlem1a  22441  ovolunlem1  22442  ovoliunlem1  22447  ovoliunlem2  22448  ovoliun  22450  ovolshftlem1  22454  ovolscalem1  22458  ovolicc1  22461  iunmbl  22498  ioombl1lem1  22503  uniioombllem2  22532  uniioombllem2OLD  22533  uniioombllem3  22535  volsup2  22555  volcn  22556  vitalilem4  22561  vitalilem5  22562  mbfconst  22583  ismbfcn2  22587  mbfeqalem  22590  mbfss  22594  mbfmulc2re  22596  mbfmax  22597  mbfneg  22598  mbfpos  22599  mbfposr  22600  mbfposb  22601  mbfadd  22609  mbfmulc2  22611  mbfsup  22612  mbfinf  22613  mbfinfOLD  22614  mbflimsup  22615  mbflimsupOLD  22616  mbflimlem  22617  mbflim  22618  i1f1lem  22639  i1f1  22640  i1fres  22655  itg1climres  22664  mbfi1fseqlem3  22667  mbfi1fseqlem4  22668  mbfi1flimlem  22672  mbfi1flim  22673  mbfmullem2  22674  mbfmul  22676  itg2const2  22691  itg2seq  22692  itg2splitlem  22698  itg2split  22699  itg2monolem1  22700  itg2monolem2  22701  itg2monolem3  22702  itg2mono  22703  itg2i1fseq  22705  itg2i1fseq2  22706  itg2gt0  22710  itg2cnlem1  22711  itg2cnlem2  22712  itg2cn  22713  iblss  22754  itgitg1  22758  itgle  22759  itgeqa  22763  itgss3  22764  ibladdlem  22769  itgaddlem1  22772  iblabslem  22777  iblabs  22778  iblabsr  22779  iblmulc2  22780  itgmulc2lem1  22781  bddmulibl  22788  itggt0  22791  itgcn  22792  ellimc2  22824  limcmpt  22830  limcres  22833  limccnp  22838  limccnp2  22839  limcco  22840  perfdvf  22850  dvreslem  22856  dvcnp2  22866  dvaddbr  22884  dvmulbr  22885  dvcjbr  22895  dvexp  22899  dvrec  22901  dvmptres3  22902  dvmptadd  22906  dvmptmul  22907  dvmptres2  22908  dvmptcmul  22910  dvmptcj  22914  dvmptntr  22917  dvmptco  22918  dvcnvlem  22920  dvef  22924  dvferm1  22929  dvferm2  22931  rolle  22934  dvlipcn  22938  dvle  22951  dvivthlem1  22952  dvivth  22954  lhop1lem  22957  lhop1  22958  lhop2  22959  lhop  22960  dvfsumle  22965  dvfsumge  22966  dvmptrecl  22968  dvfsumrlimf  22969  dvfsumlem2  22971  dvfsumlem3  22972  ftc1lem2  22980  ftc1lem6  22985  itgsubstlem  22992  tdeglem1  22999  tdeglem4  23001  coe1mul3  23040  elply2  23142  plyf  23144  elplyd  23148  plypf1  23158  coeeq2  23188  coemullem  23196  coe1termlem  23204  dvply2g  23230  elqaalem2  23265  elqaalem2OLD  23268  taylfvallem  23305  taylf  23308  tayl0  23309  taylpfval  23312  taylpf  23313  taylthlem1  23320  taylthlem2  23321  ulmshftlem  23336  ulmshft  23337  ulmcau  23342  ulmss  23344  ulmdvlem1  23347  ulmdvlem3  23349  mtest  23351  mtestbdd  23352  itgulm2  23356  psergf  23359  radcnvlem1  23360  dvradcnv  23368  pserulm  23369  psercn2  23370  pserdvlem2  23375  abelthlem4  23381  abelthlem9  23387  pige3  23464  efif1olem4  23486  logtayl  23597  logccv  23600  loglesqrt  23690  logbf  23718  leibpi  23860  rlimcnp  23883  rlimcnp2  23884  xrlimcnp  23886  efrlim  23887  dfef2  23888  o1cxp  23892  cxp2lim  23894  amgmlem  23907  lgamgulmlem2  23947  lgamgulmlem6  23951  lgamcvg2  23972  gamcvg  23973  regamcl  23978  relgamcl  23979  basellem2  24000  basellem4  24002  basellem7  24005  basellem9  24007  sqff1o  24101  fsumvma  24133  dchrelbasd  24159  lgsfcl2  24222  lgsqrlem2  24262  lgseisenlem1  24269  lgseisenlem3  24271  lgseisenlem4  24272  chpo1ub  24310  dchrmusum2  24324  dchrvmasumiflem1  24331  dchrisum0ff  24337  dchrisum0lem1b  24345  dchrisum0lem2a  24347  logsqvma2  24373  pnt2  24443  pnt  24444  abvcxp  24445  padicabv  24460  lmif  24819  axlowdimlem15  24978  nbgraf1olem2  25162  wlkiswwlk2lem5  25415  wlknwwlknfun  25430  wlkiswwlkfun  25437  wwlkextfun  25449  clwlkisclwwlklem2a  25505  clwwlkf  25514  clwlkfclwwlk  25564  vdgrf  25618  vdgrfif  25619  frgrancvvdeqlem5  25754  numclwlk1lem2f  25812  numclwlk2lem2f  25823  efghgrpOLD  26093  ipblnfi  26489  ubthlem1  26504  minvecolem1  26508  htthlem  26562  hlimadd  26838  chscllem1  27282  hoaddcl  27403  homulcl  27404  brafn  27592  kbop  27598  cnlnadjlem2  27713  strlem3a  27897  hstrlem3a  27905  off2  28238  xppreima2  28245  fpwrelmap  28318  gsummpt2d  28545  regsumfsum  28546  gsumvsca1  28547  gsumvsca2  28548  xrge0tsmsd  28550  ordtrestNEW  28729  xrge0mulc1cn  28749  esumf1o  28873  esumadd  28880  esumcst  28886  esumpfinval  28898  esumpcvgval  28901  esumcvg  28909  esumsup  28912  measinb  29045  measdivcst  29049  mbfmco2  29089  sitgclg  29177  eulerpartlems  29195  dstfrvclim1  29312  gsumncl  29426  gsumnunsn  29427  erdszelem9  29924  indispcon  29959  cvxpcon  29967  cvmsss2  29999  cvmliftlem6  30015  cvmliftlem8  30017  cvmlift3lem3  30046  mrsubcv  30150  mrsubff  30152  mrsubrn  30153  mrsubccat  30158  elmrsubrn  30160  msubrn  30169  msubff  30170  mvhf  30198  divcnvlin  30368  iprodefisum  30378  faclimlem2  30381  faclim  30383  faclim2  30385  finixpnum  31850  ptrest  31859  poimirlem17  31877  poimirlem20  31880  poimirlem24  31884  poimirlem30  31890  broucube  31894  mblfinlem2  31898  volsupnfl  31905  mbfposadd  31908  itg2addnclem2  31914  itg2gt0cn  31917  ibladdnclem  31918  itgaddnclem1  31920  itgaddnc  31922  iblabsnclem  31925  iblabsnc  31926  iblmulc2nc  31927  itgmulc2nclem1  31928  itgmulc2nclem2  31929  itgmulc2nc  31930  itgabsnc  31931  bddiblnc  31932  itggt0cn  31934  ftc1cnnc  31936  ftc1anclem1  31937  ftc1anclem2  31938  ftc1anclem3  31939  ftc1anclem4  31940  ftc1anclem5  31941  ftc1anclem6  31942  ftc1anclem7  31943  ftc1anclem8  31944  ftc1anc  31945  areacirclem4  31955  upixp  31976  totbndbnd  32041  prdsbnd  32045  cntotbnd  32048  rrnequiv  32087  lsatlss  32487  lflnegcl  32566  lshpkrcl  32607  tendoplcl  34273  tendo0cl  34282  tendoicl  34288  cmpfiiin  35464  mzpclall  35494  mzpindd  35513  fphpdo  35585  dnnumch3  35831  kelac1  35847  dfac21  35850  itgpowd  36025  expgrowth  36548  binomcxplemradcnv  36565  binomcxplemcvg  36567  binomcxplemnotnn0  36569  rnmptc  37292  mptelpm  37296  projf1o  37330  expcnfg  37497  clim1fr1  37505  mullimc  37522  ellimcabssub0  37523  mullimcf  37529  constlimc  37530  idlimc  37532  sumnnodd  37536  neglimc  37554  addlimc  37555  0ellimcdiv  37556  cncfmptssg  37573  cncfshift  37577  cncfcompt  37586  icccncfext  37591  cncfiooiccre  37599  cxpcncf2  37604  dvsinax  37609  fperdvper  37616  dvmptresicc  37617  dvcosax  37624  ioodvbdlimc1lem1  37629  ioodvbdlimc1lem2  37630  ioodvbdlimc1lem1OLD  37631  ioodvbdlimc1lem2OLD  37632  ioodvbdlimc2lem  37634  ioodvbdlimc2lemOLD  37635  dvnmptdivc  37639  dvnxpaek  37643  dvnprodlem1  37647  dvnprodlem2  37648  dvnprodlem3  37649  itgsinexplem1  37656  iblsplit  37669  itgcoscmulx  37672  itgiccshift  37683  itgperiod  37684  itgsbtaddcnst  37685  dirkerf  37785  dirkeritg  37790  dirkercncflem2  37792  fourierdlem4  37799  fourierdlem5  37800  fourierdlem9  37804  fourierdlem14  37809  fourierdlem16  37811  fourierdlem17  37812  fourierdlem18  37813  fourierdlem21  37816  fourierdlem22  37817  fourierdlem37  37833  fourierdlem50  37846  fourierdlem51  37847  fourierdlem53  37849  fourierdlem55  37851  fourierdlem57  37853  fourierdlem58  37854  fourierdlem59  37855  fourierdlem60  37856  fourierdlem61  37857  fourierdlem67  37863  fourierdlem68  37864  fourierdlem72  37868  fourierdlem73  37869  fourierdlem74  37870  fourierdlem75  37871  fourierdlem76  37872  fourierdlem78  37874  fourierdlem80  37876  fourierdlem81  37877  fourierdlem83  37879  fourierdlem84  37880  fourierdlem88  37884  fourierdlem92  37888  fourierdlem93  37889  fourierdlem97  37893  fourierdlem101  37897  fourierdlem103  37899  fourierdlem104  37900  fourierdlem111  37907  sqwvfoura  37918  elaa2lem  37923  elaa2lemOLD  37924  etransclem1  37926  etransclem8  37933  etransclem20  37945  etransclem33  37958  etransclem35  37960  etransclem39  37964  sge0tsms  38016  sge0snmpt  38019  sge0fsummpt  38026  sge0pr  38030  sge0lessmpt  38035  sge0iunmptlemfi  38049  sge0iunmptlemre  38051  sge0iunmpt  38054  sge0rpcpnf  38057  sge0isum  38063  nnfoctbdjlem  38078  psmeasure  38094  omeiunltfirp  38125  carageniuncllem2  38128  caratheodorylem1  38132  caratheodorylem2  38133  isomenndlem  38136  hoicvr  38151  hoicvrrex  38159  ovnsupge0  38160  ovnlecvr  38161  ovnf  38166  ovn0lem  38168  ovnsubaddlem1  38173  ovnsubadd  38175  pfxf  38648  c0mgm  39213  c0mhm  39214  c0snmgmhm  39218  funcringcsetcALTV2lem3  39344  funcringcsetclem3ALTV  39367  gsumlsscl  39474  ply1mulgsum  39488  lincfsuppcl  39512  linccl  39513  lincvalsc0  39520  lcoc0  39521  linc0scn0  39522  linc1  39524  lincsum  39528  lincscm  39529  lincscmcl  39531  lcoss  39535  lincext1  39553  el0ldep  39565  lincresunit1  39576  lincresunit3  39580  lmod1zr  39592  fdivmptf  39658  refdivmptf  39659  aacllem  39846
  Copyright terms: Public domain W3C validator