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

Theorem fmptd 6035
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 2820 . 2  |-  ( ph  ->  A. x  e.  A  B  e.  C )
3 fmptd.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43fmpt 6032 . 2  |-  ( A. x  e.  A  B  e.  C  <->  F : A --> C )
52, 4sylib 198 1  |-  ( ph  ->  F : A --> C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1407    e. wcel 1844   A.wral 2756    |-> cmpt 4455   -->wf 5567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-sep 4519  ax-nul 4527  ax-pr 4632
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3063  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3741  df-if 3888  df-sn 3975  df-pr 3977  df-op 3981  df-uni 4194  df-br 4398  df-opab 4456  df-mpt 4457  df-id 4740  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838  df-iota 5535  df-fun 5573  df-fn 5574  df-f 5575  df-fv 5579
This theorem is referenced by:  fmpt3d  6036  fmptco  6045  fliftrel  6191  off  6538  caofinvl  6551  curry1f  6880  curry2f  6882  fnwelem  6901  fdiagfn  7502  resixpfo  7547  pw2f1olem  7661  mapxpen  7723  xpmapenlem  7724  unxpdomlem3  7763  fsuppmptdm  7876  fsuppmptif  7895  wdom2d  8042  cantnfp1lem1  8131  cantnfp1lem2  8132  cantnfp1lem3  8133  cantnflem1d  8141  cantnflem1  8142  cantnf  8146  cantnfp1lem1OLD  8157  cantnfp1lem2OLD  8158  cantnfp1lem3OLD  8159  cantnflem1dOLD  8164  cantnflem1OLD  8165  cantnfOLD  8168  fseqenlem1  8439  fseqenlem2  8440  dfac8clem  8447  ac5num  8451  acni2  8461  infpwfien  8477  coftr  8687  fin23lem39  8764  isf34lem2  8787  fin1a2lem12  8825  axcc2lem  8850  axdc2lem  8862  axdc3lem4  8867  pwcfsdom  8992  canthp1lem2  9063  wuncval2  9157  gruf  9221  rpnnen1lem1  11255  monoord2  12184  seqf1o  12194  ccatcl  12649  swrdcl  12702  revcl  12793  revlen  12794  ello1mpt  13495  lo1o12  13507  lo1eq  13542  rlimeq  13543  climmpt2  13547  climrecl  13557  climge0  13558  o1compt  13561  rlimcn1b  13563  rlimdiv  13619  isercoll2  13642  caurcvg2  13651  caucvg  13652  sumrblem  13684  summolem2a  13688  fsumf1o  13696  sumss  13697  fsumss  13698  fsumcl2lem  13704  fsumadd  13712  isumclim3  13727  isummulc2  13730  fsummulc2  13752  fsumrelem  13774  climfsum  13787  isumshft  13804  divcnv  13818  supcvg  13821  prodfdiv  13859  prodrblem  13890  prodmolem2a  13895  fprodf1o  13907  prodss  13908  fprodss  13909  fprodser  13910  fprodcl2lem  13911  fprodmul  13919  fproddiv  13920  fprodn0  13937  iprodclim3  13947  fprodefsum  14041  rpnnen2lem2  14160  crt  14519  eulerthlem1  14522  iserodd  14570  prmreclem2  14646  prmreclem6  14650  1arithlem3  14654  4sqlem11  14684  vdwapf  14701  vdwlem2  14711  vdwlem4  14713  vdwlem6  14715  vdwlem10  14719  ramub1lem2  14756  ramcl  14758  prdsplusg  15074  prdsmulr  15075  prdsvsca  15076  mrcflem  15222  mreacs  15274  acsfn  15275  homaf  15635  funcestrcsetclem3  15737  funcsetcestrclem3  15751  prfcl  15798  curf1cl  15823  hofcllem  15853  hofcl  15854  yonedalem3a  15869  yonedalem4c  15872  yonedainv  15876  prdspjmhm  16324  pwsco1mhm  16327  pwsco2mhm  16328  gsumz  16331  gsumwspan  16340  vrmdfval  16350  vrmdf  16352  frmdup1  16358  grpinvf  16420  cycsubgcl  16553  cycsubgss  16554  conjghm  16623  conjnmz  16626  qusghm  16629  galactghm  16754  symgextf  16768  symgfixf  16787  pmtrf  16806  pmtrdifwrdellem1  16832  psgnunilem5  16845  odf1  16910  dfod2  16912  odf1o2  16919  pgpssslw  16960  sylow2blem1  16966  pj1f  17041  frgpmhm  17109  vrgpf  17112  mulgmhm  17162  mulgghm  17163  iscyggen2  17210  cyggenod  17213  iscyg3  17215  gsummptfsadd  17266  gsummptfsaddOLD  17267  gsumzsplit  17270  gsumzsplitOLD  17271  gsumsplit2  17274  gsummptfidmsplitres  17276  gsumconst  17279  gsummptshft  17281  gsummhm2  17286  gsummhm2OLD  17287  gsummptmhm  17288  gsummptfidminv  17297  gsummptfssub  17299  gsumzunsnd  17305  gsummptf1o  17313  gsummpt1n0  17315  gsum2dlem1  17320  gsum2dlem2  17321  gsum2d  17322  gsum2dOLD  17323  prdsgsum  17329  prdsgsumOLD  17330  dprdfeq0  17384  dprdfeq0OLD  17391  dprdlub  17395  dprdz  17399  dprd2dlem1  17412  dprd2da  17413  ablfac1b  17443  ablfac2  17462  srglmhm  17508  srgrmhm  17509  ringlghm  17572  ringrghm  17573  gsumdixpOLD  17579  gsumdixp  17580  abvtrivd  17811  issrngd  17832  lmodvsghm  17893  lspf  17942  pwssplit0  18026  asclf  18308  snifpsrbag  18337  psrass1lem  18351  psrbasOLD  18353  psrmulcllem  18362  psr1cl  18377  psrlidm  18378  psrlidmOLD  18379  psrridm  18380  psrridmOLD  18381  psrcom  18386  resspsrmul  18394  subrgpsr  18396  mvridlemOLD  18397  mvrf  18402  mplmon  18447  mplmonmul  18448  mplcoe1  18449  mplcoe3OLD  18451  mplcoe5lem  18452  mplcoe5  18453  mplcoe2OLD  18455  mplbas2  18456  mplbas2OLD  18457  psrbagsn  18482  evlslem4OLD  18495  evlslem4  18496  evlslem2  18502  evlslem6  18503  evlslem6OLD  18504  evlslem3  18505  evlslem1  18506  evlsval2  18511  psropprmul  18601  coe1mul2  18632  coe1tmmul2  18639  coe1tmmul  18640  ply1coe  18659  ply1coeOLD  18660  gsumsmonply1  18667  gsummoncoe1  18668  gsumfsum  18806  expmhm  18807  expghm  18835  mulgghm2  18836  evpmodpmf1o  18932  isphld  18989  pjff  19043  frlmgsumOLD  19099  frlmgsum  19100  frlmsplit2  19101  frlmphl  19110  uvcff  19120  uvcresum  19122  frlmup1  19127  mamulid  19237  mamurid  19238  scmatf  19325  mdetf  19391  mdetunilem9  19416  mdetuni0  19417  mdetmul  19419  maduf  19437  smadiadetlem3lem1  19462  cpm2mf  19547  m2cpmfo  19551  pmatcollpw1  19571  pmatcollpw3lem  19578  pmatcollpw3fi1lem1  19581  pmatcollpw3fi1lem2  19582  pm2mpcl  19592  mply1topmatcl  19600  mp2pm2mplem2  19602  mp2pm2mp  19606  pm2mpmhmlem2  19614  chfacfisf  19649  chfacfisfcpmat  19650  cpmidpmatlem2  19666  cayhamlem4  19683  pptbas  19803  tgrest  19955  resttopon  19957  rest0  19965  restfpw  19975  ordtbaslem  19984  ordtuni  19986  ordtrest  19998  cnpfval  20030  pnrmopn  20139  cncmp  20187  discmp  20193  1stcfb  20240  2ndcomap  20253  dis2ndc  20255  lly1stc  20291  comppfsc  20327  kgencmp  20340  ptpjpre1  20366  ptpjcn  20406  ptcldmpt  20409  ptclsg  20410  dfac14  20413  xkoccn  20414  txcnp  20415  ptcnp  20417  txcnmpt  20419  uptx  20420  ptcn  20422  ptrescn  20434  txlm  20443  xkoptsub  20449  xkoco1cn  20452  xkoco2cn  20453  cnmpt11  20458  xkoinjcn  20482  kqffn  20520  pt1hmeo  20601  fbasrn  20679  trfilss  20684  trfg  20686  rnelfmlem  20747  txflf  20801  flfcnp2  20802  fclscmpi  20824  alexsublem  20838  ptcmplem3  20848  symgtgp  20894  subgntr  20899  opnsubg  20900  clsnsg  20902  tgpconcomp  20905  tsmsfbas  20920  eltsms  20925  haustsms  20928  tsmscls  20930  tsms0  20937  tsmsmhm  20942  tgptsmscls  20946  tsmssplit  20948  tsmsxplem1  20949  tsmsxplem2  20950  ustuqtop0  21037  prdsdsf  21164  prdsxmetlem  21165  imasdsf1olem  21170  prdsbl  21288  stdbdxmet  21312  met1stc  21318  nmf2  21407  nmof  21520  xrge0gsumle  21632  xrge0tsms  21633  metdsf  21646  metdsge  21647  mulc1cncf  21703  cncfmpt2ss  21713  cnmptre  21721  evth  21753  evth2  21754  lebnumlem1  21755  cphnmf  21936  tchcph  21974  cmetcaulem  22021  rrxmval  22126  minveclem1  22133  minveclem3b  22137  ovollb2lem  22193  ovolctb  22195  ovolunlem1a  22201  ovolunlem1  22202  ovoliunlem1  22207  ovoliunlem2  22208  ovoliun  22210  ovolshftlem1  22214  ovolscalem1  22218  ovolicc1  22221  iunmbl  22257  ioombl1lem1  22262  uniioombllem2  22286  uniioombllem3  22288  volsup2  22308  volcn  22309  vitalilem4  22314  vitalilem5  22315  mbfconst  22336  ismbfcn2  22340  mbfeqalem  22343  mbfss  22347  mbfmulc2re  22349  mbfmax  22350  mbfneg  22351  mbfpos  22352  mbfposr  22353  mbfposb  22354  mbfadd  22362  mbfmulc2  22364  mbfsup  22365  mbfinf  22366  mbflimsup  22367  mbflimlem  22368  mbflim  22369  i1f1lem  22390  i1f1  22391  i1fres  22406  itg1climres  22415  mbfi1fseqlem3  22418  mbfi1fseqlem4  22419  mbfi1flimlem  22423  mbfi1flim  22424  mbfmullem2  22425  mbfmul  22427  itg2const2  22442  itg2seq  22443  itg2splitlem  22449  itg2split  22450  itg2monolem1  22451  itg2monolem2  22452  itg2monolem3  22453  itg2mono  22454  itg2i1fseq  22456  itg2i1fseq2  22457  itg2gt0  22461  itg2cnlem1  22462  itg2cnlem2  22463  itg2cn  22464  iblss  22505  itgitg1  22509  itgle  22510  itgeqa  22514  itgss3  22515  ibladdlem  22520  itgaddlem1  22523  iblabslem  22528  iblabs  22529  iblabsr  22530  iblmulc2  22531  itgmulc2lem1  22532  bddmulibl  22539  itggt0  22542  itgcn  22543  ellimc2  22575  limcmpt  22581  limcres  22584  limccnp  22589  limccnp2  22590  limcco  22591  perfdvf  22601  dvreslem  22607  dvcnp2  22617  dvaddbr  22635  dvmulbr  22636  dvcjbr  22646  dvexp  22650  dvrec  22652  dvmptres3  22653  dvmptadd  22657  dvmptmul  22658  dvmptres2  22659  dvmptcmul  22661  dvmptcj  22665  dvmptntr  22668  dvmptco  22669  dvcnvlem  22671  dvef  22675  dvferm1  22680  dvferm2  22682  rolle  22685  dvlipcn  22689  dvle  22702  dvivthlem1  22703  dvivth  22705  lhop1lem  22708  lhop1  22709  lhop2  22710  lhop  22711  dvfsumle  22716  dvfsumge  22717  dvmptrecl  22719  dvfsumrlimf  22720  dvfsumlem2  22722  dvfsumlem3  22723  ftc1lem2  22731  ftc1lem6  22736  itgsubstlem  22743  tdeglem1  22750  tdeglem4  22752  coe1mul3  22794  elply2  22887  plyf  22889  elplyd  22893  plypf1  22903  coeeq2  22933  coemullem  22941  coe1termlem  22949  dvply2g  22975  elqaalem2  23010  taylfvallem  23047  taylf  23050  tayl0  23051  taylpfval  23054  taylpf  23055  taylthlem1  23062  taylthlem2  23063  ulmshftlem  23078  ulmshft  23079  ulmcau  23084  ulmss  23086  ulmdvlem1  23089  ulmdvlem3  23091  mtest  23093  mtestbdd  23094  itgulm2  23098  psergf  23101  radcnvlem1  23102  dvradcnv  23110  pserulm  23111  psercn2  23112  pserdvlem2  23117  abelthlem4  23123  abelthlem9  23129  pige3  23204  efif1olem4  23226  logtayl  23337  logccv  23340  loglesqrt  23430  logbf  23458  leibpi  23600  rlimcnp  23623  rlimcnp2  23624  xrlimcnp  23626  efrlim  23627  dfef2  23628  o1cxp  23632  cxp2lim  23634  amgmlem  23647  lgamgulmlem2  23687  lgamgulmlem6  23691  lgamcvg2  23712  gamcvg  23713  regamcl  23718  relgamcl  23719  basellem2  23738  basellem4  23740  basellem7  23743  basellem9  23745  sqff1o  23839  fsumvma  23871  dchrelbasd  23897  lgsfcl2  23960  lgsqrlem2  24000  lgseisenlem1  24007  lgseisenlem3  24009  lgseisenlem4  24010  chpo1ub  24048  dchrmusum2  24062  dchrvmasumiflem1  24069  dchrisum0ff  24075  dchrisum0lem1b  24083  dchrisum0lem2a  24085  logsqvma2  24111  pnt2  24181  pnt  24182  abvcxp  24183  padicabv  24198  lmif  24546  axlowdimlem15  24688  nbgraf1olem2  24871  wlkiswwlk2lem5  25124  wlknwwlknfun  25139  wlkiswwlkfun  25146  wwlkextfun  25158  clwlkisclwwlklem2a  25214  clwwlkf  25223  clwlkfclwwlk  25273  vdgrf  25327  vdgrfif  25328  frgrancvvdeqlem5  25463  numclwlk1lem2f  25521  numclwlk2lem2f  25532  efghgrpOLD  25802  ipblnfi  26198  ubthlem1  26213  minvecolem1  26217  htthlem  26261  hlimadd  26537  chscllem1  26982  hoaddcl  27103  homulcl  27104  brafn  27292  kbop  27298  cnlnadjlem2  27413  strlem3a  27597  hstrlem3a  27605  off2  27937  xppreima2  27944  fpwrelmap  28016  gsummpt2d  28236  regsumfsum  28237  gsumvsca1  28238  gsumvsca2  28239  xrge0tsmsd  28241  ordtrestNEW  28369  xrge0mulc1cn  28389  esumf1o  28510  esumadd  28517  esumcst  28523  esumpfinval  28535  esumpcvgval  28538  esumcvg  28546  esumsup  28549  measinb  28682  measdivcst  28686  mbfmco2  28726  sitgclg  28803  eulerpartlems  28818  dstfrvclim1  28935  gsumncl  29011  gsumnunsn  29012  erdszelem9  29509  indispcon  29544  cvxpcon  29552  cvmsss2  29584  cvmliftlem6  29600  cvmliftlem8  29602  cvmlift3lem3  29631  mrsubcv  29735  mrsubff  29737  mrsubrn  29738  mrsubccat  29743  elmrsubrn  29745  msubrn  29754  msubff  29755  mvhf  29783  divcnvlin  29953  iprodefisum  29963  faclimlem2  29966  faclim  29968  faclim2  29970  finixpnum  31423  ptrest  31433  mblfinlem2  31437  volsupnfl  31444  mbfposadd  31447  itg2addnclem2  31453  itg2gt0cn  31456  ibladdnclem  31457  itgaddnclem1  31459  itgaddnc  31461  iblabsnclem  31464  iblabsnc  31465  iblmulc2nc  31466  itgmulc2nclem1  31467  itgmulc2nclem2  31468  itgmulc2nc  31469  itgabsnc  31470  bddiblnc  31471  itggt0cn  31473  ftc1cnnc  31475  ftc1anclem1  31476  ftc1anclem2  31477  ftc1anclem3  31478  ftc1anclem4  31479  ftc1anclem5  31480  ftc1anclem6  31481  ftc1anclem7  31482  ftc1anclem8  31483  ftc1anc  31484  areacirclem4  31494  upixp  31515  totbndbnd  31580  prdsbnd  31584  cntotbnd  31587  rrnequiv  31626  lsatlss  32027  lflnegcl  32106  lshpkrcl  32147  tendoplcl  33813  tendo0cl  33822  tendoicl  33828  cmpfiiin  35004  mzpclall  35034  mzpindd  35053  fphpdo  35125  dnnumch3  35368  kelac1  35384  dfac21  35387  itgpowd  35559  expgrowth  36101  binomcxplemradcnv  36118  binomcxplemcvg  36120  binomcxplemnotnn0  36122  rnmptc  36837  mptelpm  36841  expcnfg  36967  clim1fr1  36988  mullimc  37003  ellimcabssub0  37004  mullimcf  37010  constlimc  37011  idlimc  37013  sumnnodd  37017  neglimc  37034  addlimc  37035  0ellimcdiv  37036  cncfmptssg  37053  cncfshift  37057  cncfcompt  37066  icccncfext  37071  cncfiooiccre  37079  cxpcncf2  37084  dvsinax  37089  fperdvper  37096  dvmptresicc  37097  dvcosax  37104  ioodvbdlimc1lem1  37109  ioodvbdlimc1lem2  37110  ioodvbdlimc2lem  37112  dvnmptdivc  37116  dvnxpaek  37120  dvnprodlem1  37124  dvnprodlem2  37125  dvnprodlem3  37126  itgsinexplem1  37133  iblsplit  37146  itgcoscmulx  37149  itgiccshift  37160  itgperiod  37161  itgsbtaddcnst  37162  dirkerf  37260  dirkeritg  37265  dirkercncflem2  37267  fourierdlem4  37274  fourierdlem5  37275  fourierdlem9  37279  fourierdlem14  37284  fourierdlem16  37286  fourierdlem17  37287  fourierdlem18  37288  fourierdlem21  37291  fourierdlem22  37292  fourierdlem37  37307  fourierdlem50  37320  fourierdlem51  37321  fourierdlem53  37323  fourierdlem55  37325  fourierdlem57  37327  fourierdlem58  37328  fourierdlem59  37329  fourierdlem60  37330  fourierdlem61  37331  fourierdlem67  37337  fourierdlem68  37338  fourierdlem72  37342  fourierdlem73  37343  fourierdlem74  37344  fourierdlem75  37345  fourierdlem76  37346  fourierdlem78  37348  fourierdlem80  37350  fourierdlem81  37351  fourierdlem83  37353  fourierdlem84  37354  fourierdlem88  37358  fourierdlem92  37362  fourierdlem93  37363  fourierdlem97  37367  fourierdlem101  37371  fourierdlem103  37373  fourierdlem104  37374  fourierdlem111  37381  sqwvfoura  37392  elaa2lem  37397  etransclem1  37399  etransclem8  37406  etransclem20  37418  etransclem33  37431  etransclem35  37433  etransclem39  37437  pfxf  37889  c0mgm  38239  c0mhm  38240  c0snmgmhm  38244  funcringcsetcALTV2lem3  38370  funcringcsetclem3ALTV  38393  gsumlsscl  38500  ply1mulgsum  38514  lincfsuppcl  38538  linccl  38539  lincvalsc0  38546  lcoc0  38547  linc0scn0  38548  linc1  38550  lincsum  38554  lincscm  38555  lincscmcl  38557  lcoss  38561  lincext1  38579  el0ldep  38591  lincresunit1  38602  lincresunit3  38606  lmod1zr  38618  fdivmptf  38685  refdivmptf  38686  aacllem  38873
  Copyright terms: Public domain W3C validator