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

Theorem fmptd 6046
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 2802 . 2  |-  ( ph  ->  A. x  e.  A  B  e.  C )
3 fmptd.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43fmpt 6043 . 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 1444    e. wcel 1887   A.wral 2737    |-> cmpt 4461   -->wf 5578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pr 4639
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-fv 5590
This theorem is referenced by:  fmpt3d  6047  fmptco  6056  fliftrel  6201  off  6546  caofinvl  6558  curry1f  6890  curry2f  6892  fnwelem  6911  fdiagfn  7515  resixpfo  7560  pw2f1olem  7676  mapxpen  7738  xpmapenlem  7739  unxpdomlem3  7778  fsuppmptdm  7894  fsuppmptif  7913  wdom2d  8095  cantnfp1lem1  8183  cantnfp1lem2  8184  cantnfp1lem3  8185  cantnflem1d  8193  cantnflem1  8194  cantnf  8198  fseqenlem1  8455  fseqenlem2  8456  dfac8clem  8463  ac5num  8467  acni2  8477  infpwfien  8493  coftr  8703  fin23lem39  8780  isf34lem2  8803  fin1a2lem12  8841  axcc2lem  8866  axdc2lem  8878  axdc3lem4  8883  pwcfsdom  9008  canthp1lem2  9078  wuncval2  9172  gruf  9236  rpnnen1lem1  11290  monoord2  12244  seqf1o  12254  ccatcl  12720  swrdcl  12775  revcl  12866  revlen  12867  ello1mpt  13585  lo1o12  13597  lo1eq  13632  rlimeq  13633  climmpt2  13637  climrecl  13647  climge0  13648  o1compt  13651  rlimcn1b  13653  rlimdiv  13709  isercoll2  13732  caurcvg2  13744  caucvg  13745  sumrblem  13777  summolem2a  13781  fsumf1o  13789  sumss  13790  fsumss  13791  fsumcl2lem  13797  fsumadd  13805  isumclim3  13820  isummulc2  13823  fsummulc2  13845  fsumrelem  13867  climfsum  13880  isumshft  13897  divcnv  13911  supcvg  13914  prodfdiv  13952  prodrblem  13983  prodmolem2a  13988  fprodf1o  14000  prodss  14001  fprodss  14002  fprodser  14003  fprodcl2lem  14004  fprodmul  14014  fproddiv  14015  fprodn0  14033  iprodclim3  14053  fprodefsum  14149  rpnnen2lem2  14268  crt  14726  eulerthlem1  14729  iserodd  14785  prmreclem2  14861  prmreclem6  14865  1arithlem3  14869  4sqlem11  14899  vdwapf  14922  vdwlem2  14932  vdwlem4  14934  vdwlem6  14936  vdwlem10  14940  ramub1lem2  14985  ramcl  14987  prmodvdslcmf  15005  prmordvdslcmfOLD  15019  prmordvdslcmsOLDOLD  15021  prmgaplcm  15031  prdsplusg  15356  prdsmulr  15357  prdsvsca  15358  mrcflem  15512  mreacs  15564  acsfn  15565  homaf  15925  funcestrcsetclem3  16027  funcsetcestrclem3  16041  prfcl  16088  curf1cl  16113  hofcllem  16143  hofcl  16144  yonedalem3a  16159  yonedalem4c  16162  yonedainv  16166  prdspjmhm  16614  pwsco1mhm  16617  pwsco2mhm  16618  gsumz  16621  gsumwspan  16630  vrmdfval  16640  vrmdf  16642  frmdup1  16648  grpinvf  16710  cycsubgcl  16843  cycsubgss  16844  conjghm  16913  conjnmz  16916  qusghm  16919  galactghm  17044  symgextf  17058  symgfixf  17077  pmtrf  17096  pmtrdifwrdellem1  17122  psgnunilem5  17135  odf1  17213  dfod2  17215  odf1o2  17222  pgpssslw  17266  sylow2blem1  17272  pj1f  17347  frgpmhm  17415  vrgpf  17418  mulgmhm  17468  mulgghm  17469  iscyggen2  17516  cyggenod  17519  iscyg3  17521  gsummptfsadd  17557  gsumzsplit  17560  gsumsplit2  17562  gsummptfidmsplitres  17564  gsumconst  17567  gsummptshft  17569  gsummhm2  17572  gsummptmhm  17573  gsummptfidminv  17580  gsummptfssub  17582  gsumzunsnd  17588  gsummptf1o  17595  gsummpt1n0  17597  gsum2dlem1  17602  gsum2dlem2  17603  gsum2d  17604  prdsgsum  17610  dprdfeq0  17655  dprdlub  17659  dprdz  17663  dprd2dlem1  17674  dprd2da  17675  ablfac1b  17703  ablfac2  17722  srglmhm  17768  srgrmhm  17769  ringlghm  17832  ringrghm  17833  gsumdixp  17837  abvtrivd  18068  issrngd  18089  lmodvsghm  18149  lspf  18197  pwssplit0  18281  asclf  18561  snifpsrbag  18590  psrass1lem  18601  psrmulcllem  18611  psr1cl  18626  psrlidm  18627  psrridm  18628  psrcom  18633  resspsrmul  18641  subrgpsr  18643  mvrf  18648  mplmon  18687  mplmonmul  18688  mplcoe1  18689  mplcoe5lem  18691  mplcoe5  18692  mplbas2  18694  psrbagsn  18718  evlslem4  18731  evlslem2  18735  evlslem6  18736  evlslem3  18737  evlslem1  18738  evlsval2  18743  psropprmul  18831  coe1mul2  18862  coe1tmmul2  18869  coe1tmmul  18870  ply1coe  18889  ply1coeOLD  18890  gsumsmonply1  18897  gsummoncoe1  18898  gsumfsum  19034  regsumfsum  19035  expmhm  19036  expghm  19067  mulgghm2  19068  evpmodpmf1o  19164  isphld  19221  pjff  19275  frlmgsum  19330  frlmsplit2  19331  frlmphl  19339  uvcff  19349  uvcresum  19351  frlmup1  19356  mamulid  19466  mamurid  19467  scmatf  19554  mdetf  19620  mdetunilem9  19645  mdetuni0  19646  mdetmul  19648  maduf  19666  smadiadetlem3lem1  19691  cpm2mf  19776  m2cpmfo  19780  pmatcollpw1  19800  pmatcollpw3lem  19807  pmatcollpw3fi1lem1  19810  pmatcollpw3fi1lem2  19811  pm2mpcl  19821  mply1topmatcl  19829  mp2pm2mplem2  19831  mp2pm2mp  19835  pm2mpmhmlem2  19843  chfacfisf  19878  chfacfisfcpmat  19879  cpmidpmatlem2  19895  cayhamlem4  19912  pptbas  20023  tgrest  20175  resttopon  20177  rest0  20185  restfpw  20195  ordtbaslem  20204  ordtuni  20206  ordtrest  20218  cnpfval  20250  pnrmopn  20359  cncmp  20407  discmp  20413  1stcfb  20460  2ndcomap  20473  dis2ndc  20475  lly1stc  20511  comppfsc  20547  kgencmp  20560  ptpjpre1  20586  ptpjcn  20626  ptcldmpt  20629  ptclsg  20630  dfac14  20633  xkoccn  20634  txcnp  20635  ptcnp  20637  txcnmpt  20639  uptx  20640  ptcn  20642  ptrescn  20654  txlm  20663  xkoptsub  20669  xkoco1cn  20672  xkoco2cn  20673  cnmpt11  20678  xkoinjcn  20702  kqffn  20740  pt1hmeo  20821  fbasrn  20899  trfilss  20904  trfg  20906  rnelfmlem  20967  txflf  21021  flfcnp2  21022  fclscmpi  21044  alexsublem  21059  ptcmplem3  21069  symgtgp  21116  subgntr  21121  opnsubg  21122  clsnsg  21124  tgpconcomp  21127  tsmsfbas  21142  eltsms  21147  haustsms  21150  tsmscls  21152  tsms0  21156  tsmsmhm  21160  tgptsmscls  21164  tsmssplit  21166  tsmsxplem1  21167  tsmsxplem2  21168  ustuqtop0  21255  prdsdsf  21382  prdsxmetlem  21383  imasdsf1olem  21388  prdsbl  21506  stdbdxmet  21530  met1stc  21536  nmf2  21607  nmofOLD  21742  xrge0gsumle  21851  xrge0tsms  21852  metdsf  21865  metdsge  21866  metdsfOLD  21880  metdsgeOLD  21881  mulc1cncf  21937  cncfmpt2ss  21947  cnmptre  21955  evth  21987  evth2  21988  lebnumlem1  21989  lebnumlem1OLD  21992  cphnmf  22173  tchcph  22211  cmetcaulem  22258  rrxmval  22359  minveclem1  22366  minveclem3b  22370  minveclem3bOLD  22382  ovollb2lem  22441  ovolctb  22443  ovolunlem1a  22449  ovolunlem1  22450  ovoliunlem1  22455  ovoliunlem2  22456  ovoliun  22458  ovolshftlem1  22462  ovolscalem1  22466  ovolicc1  22469  iunmbl  22506  ioombl1lem1  22511  uniioombllem2  22540  uniioombllem2OLD  22541  uniioombllem3  22543  volsup2  22563  volcn  22564  vitalilem4  22569  vitalilem5  22570  mbfconst  22591  ismbfcn2  22595  mbfeqalem  22598  mbfss  22602  mbfmulc2re  22604  mbfmax  22605  mbfneg  22606  mbfpos  22607  mbfposr  22608  mbfposb  22609  mbfadd  22617  mbfmulc2  22619  mbfsup  22620  mbfinf  22621  mbfinfOLD  22622  mbflimsup  22623  mbflimsupOLD  22624  mbflimlem  22625  mbflim  22626  i1f1lem  22647  i1f1  22648  i1fres  22663  itg1climres  22672  mbfi1fseqlem3  22675  mbfi1fseqlem4  22676  mbfi1flimlem  22680  mbfi1flim  22681  mbfmullem2  22682  mbfmul  22684  itg2const2  22699  itg2seq  22700  itg2splitlem  22706  itg2split  22707  itg2monolem1  22708  itg2monolem2  22709  itg2monolem3  22710  itg2mono  22711  itg2i1fseq  22713  itg2i1fseq2  22714  itg2gt0  22718  itg2cnlem1  22719  itg2cnlem2  22720  itg2cn  22721  iblss  22762  itgitg1  22766  itgle  22767  itgeqa  22771  itgss3  22772  ibladdlem  22777  itgaddlem1  22780  iblabslem  22785  iblabs  22786  iblabsr  22787  iblmulc2  22788  itgmulc2lem1  22789  bddmulibl  22796  itggt0  22799  itgcn  22800  ellimc2  22832  limcmpt  22838  limcres  22841  limccnp  22846  limccnp2  22847  limcco  22848  perfdvf  22858  dvreslem  22864  dvcnp2  22874  dvaddbr  22892  dvmulbr  22893  dvcjbr  22903  dvexp  22907  dvrec  22909  dvmptres3  22910  dvmptadd  22914  dvmptmul  22915  dvmptres2  22916  dvmptcmul  22918  dvmptcj  22922  dvmptntr  22925  dvmptco  22926  dvcnvlem  22928  dvef  22932  dvferm1  22937  dvferm2  22939  rolle  22942  dvlipcn  22946  dvle  22959  dvivthlem1  22960  dvivth  22962  lhop1lem  22965  lhop1  22966  lhop2  22967  lhop  22968  dvfsumle  22973  dvfsumge  22974  dvmptrecl  22976  dvfsumrlimf  22977  dvfsumlem2  22979  dvfsumlem3  22980  ftc1lem2  22988  ftc1lem6  22993  itgsubstlem  23000  tdeglem1  23007  tdeglem4  23009  coe1mul3  23048  elply2  23150  plyf  23152  elplyd  23156  plypf1  23166  coeeq2  23196  coemullem  23204  coe1termlem  23212  dvply2g  23238  elqaalem2  23273  elqaalem2OLD  23276  taylfvallem  23313  taylf  23316  tayl0  23317  taylpfval  23320  taylpf  23321  taylthlem1  23328  taylthlem2  23329  ulmshftlem  23344  ulmshft  23345  ulmcau  23350  ulmss  23352  ulmdvlem1  23355  ulmdvlem3  23357  mtest  23359  mtestbdd  23360  itgulm2  23364  psergf  23367  radcnvlem1  23368  dvradcnv  23376  pserulm  23377  psercn2  23378  pserdvlem2  23383  abelthlem4  23389  abelthlem9  23395  pige3  23472  efif1olem4  23494  logtayl  23605  logccv  23608  loglesqrt  23698  logbf  23726  leibpi  23868  rlimcnp  23891  rlimcnp2  23892  xrlimcnp  23894  efrlim  23895  dfef2  23896  o1cxp  23900  cxp2lim  23902  amgmlem  23915  lgamgulmlem2  23955  lgamgulmlem6  23959  lgamcvg2  23980  gamcvg  23981  regamcl  23986  relgamcl  23987  basellem2  24008  basellem4  24010  basellem7  24013  basellem9  24015  sqff1o  24109  fsumvma  24141  dchrelbasd  24167  lgsfcl2  24230  lgsqrlem2  24270  lgseisenlem1  24277  lgseisenlem3  24279  lgseisenlem4  24280  chpo1ub  24318  dchrmusum2  24332  dchrvmasumiflem1  24339  dchrisum0ff  24345  dchrisum0lem1b  24353  dchrisum0lem2a  24355  logsqvma2  24381  pnt2  24451  pnt  24452  abvcxp  24453  padicabv  24468  lmif  24827  axlowdimlem15  24986  nbgraf1olem2  25170  wlkiswwlk2lem5  25423  wlknwwlknfun  25438  wlkiswwlkfun  25445  wwlkextfun  25457  clwlkisclwwlklem2a  25513  clwwlkf  25522  clwlkfclwwlk  25572  vdgrf  25626  vdgrfif  25627  frgrancvvdeqlem5  25762  numclwlk1lem2f  25820  numclwlk2lem2f  25831  efghgrpOLD  26101  ipblnfi  26497  ubthlem1  26512  minvecolem1  26516  htthlem  26570  hlimadd  26846  chscllem1  27290  hoaddcl  27411  homulcl  27412  brafn  27600  kbop  27606  cnlnadjlem2  27721  strlem3a  27905  hstrlem3a  27913  off2  28242  xppreima2  28249  fpwrelmap  28318  gsummpt2d  28544  gsumvsca1  28545  gsumvsca2  28546  xrge0tsmsd  28548  ordtrestNEW  28727  xrge0mulc1cn  28747  esumf1o  28871  esumadd  28878  esumcst  28884  esumpfinval  28896  esumpcvgval  28899  esumcvg  28907  esumsup  28910  measinb  29043  measdivcst  29047  mbfmco2  29087  sitgclg  29175  eulerpartlems  29193  dstfrvclim1  29310  gsumncl  29424  gsumnunsn  29425  erdszelem9  29922  indispcon  29957  cvxpcon  29965  cvmsss2  29997  cvmliftlem6  30013  cvmliftlem8  30015  cvmlift3lem3  30044  mrsubcv  30148  mrsubff  30150  mrsubrn  30151  mrsubccat  30156  elmrsubrn  30158  msubrn  30167  msubff  30168  mvhf  30196  divcnvlin  30367  iprodefisum  30377  faclimlem2  30380  faclim  30382  faclim2  30384  finixpnum  31930  ptrest  31939  poimirlem17  31957  poimirlem20  31960  poimirlem24  31964  poimirlem30  31970  broucube  31974  mblfinlem2  31978  volsupnfl  31985  mbfposadd  31988  itg2addnclem2  31994  itg2gt0cn  31997  ibladdnclem  31998  itgaddnclem1  32000  itgaddnc  32002  iblabsnclem  32005  iblabsnc  32006  iblmulc2nc  32007  itgmulc2nclem1  32008  itgmulc2nclem2  32009  itgmulc2nc  32010  itgabsnc  32011  bddiblnc  32012  itggt0cn  32014  ftc1cnnc  32016  ftc1anclem1  32017  ftc1anclem2  32018  ftc1anclem3  32019  ftc1anclem4  32020  ftc1anclem5  32021  ftc1anclem6  32022  ftc1anclem7  32023  ftc1anclem8  32024  ftc1anc  32025  areacirclem4  32035  upixp  32056  totbndbnd  32121  prdsbnd  32125  cntotbnd  32128  rrnequiv  32167  lsatlss  32562  lflnegcl  32641  lshpkrcl  32682  tendoplcl  34348  tendo0cl  34357  tendoicl  34363  cmpfiiin  35539  mzpclall  35569  mzpindd  35588  fphpdo  35660  dnnumch3  35905  kelac1  35921  dfac21  35924  itgpowd  36099  expgrowth  36684  binomcxplemradcnv  36701  binomcxplemcvg  36703  binomcxplemnotnn0  36705  rnmptc  37437  mptelpm  37441  projf1o  37474  expcnfg  37671  clim1fr1  37679  mullimc  37696  ellimcabssub0  37697  mullimcf  37703  constlimc  37704  idlimc  37706  sumnnodd  37710  neglimc  37728  addlimc  37729  0ellimcdiv  37730  cncfmptssg  37747  cncfshift  37751  cncfcompt  37760  icccncfext  37765  cncfiooiccre  37773  cxpcncf2  37778  dvsinax  37783  fperdvper  37790  dvmptresicc  37791  dvcosax  37798  ioodvbdlimc1lem1  37803  ioodvbdlimc1lem2  37804  ioodvbdlimc1lem1OLD  37805  ioodvbdlimc1lem2OLD  37806  ioodvbdlimc2lem  37808  ioodvbdlimc2lemOLD  37809  dvnmptdivc  37813  dvnxpaek  37817  dvnprodlem1  37821  dvnprodlem2  37822  dvnprodlem3  37823  itgsinexplem1  37830  iblsplit  37843  itgcoscmulx  37846  itgiccshift  37857  itgperiod  37858  itgsbtaddcnst  37859  dirkerf  37959  dirkeritg  37964  dirkercncflem2  37966  fourierdlem4  37973  fourierdlem5  37974  fourierdlem9  37978  fourierdlem14  37983  fourierdlem16  37985  fourierdlem17  37986  fourierdlem18  37987  fourierdlem21  37990  fourierdlem22  37991  fourierdlem37  38007  fourierdlem50  38020  fourierdlem51  38021  fourierdlem53  38023  fourierdlem55  38025  fourierdlem57  38027  fourierdlem58  38028  fourierdlem59  38029  fourierdlem60  38030  fourierdlem61  38031  fourierdlem67  38037  fourierdlem68  38038  fourierdlem72  38042  fourierdlem73  38043  fourierdlem74  38044  fourierdlem75  38045  fourierdlem76  38046  fourierdlem78  38048  fourierdlem80  38050  fourierdlem81  38051  fourierdlem83  38053  fourierdlem84  38054  fourierdlem88  38058  fourierdlem92  38062  fourierdlem93  38063  fourierdlem97  38067  fourierdlem101  38071  fourierdlem103  38073  fourierdlem104  38074  fourierdlem111  38081  sqwvfoura  38092  elaa2lem  38097  elaa2lemOLD  38098  etransclem1  38100  etransclem8  38107  etransclem20  38119  etransclem33  38132  etransclem35  38134  etransclem39  38138  rrxtopnfi  38155  sge0tsms  38222  sge0snmpt  38225  sge0fsummpt  38232  sge0pr  38236  sge0lessmpt  38241  sge0iunmptlemfi  38255  sge0iunmptlemre  38257  sge0iunmpt  38260  sge0rpcpnf  38263  sge0isum  38269  nnfoctbdjlem  38293  psmeasure  38309  omeiunltfirp  38340  carageniuncllem2  38343  caratheodorylem1  38347  caratheodorylem2  38348  isomenndlem  38351  hoicvr  38370  hoicvrrex  38378  ovnsupge0  38379  ovnlecvr  38380  ovnf  38385  ovn0lem  38387  ovnsubaddlem1  38392  ovnsubadd  38394  hsphoif  38398  sge0hsphoire  38411  hoidmv1lelem1  38413  hoidmv1lelem2  38414  hoidmv1lelem3  38415  hoidmv1le  38416  hoidmvlelem1  38417  hoidmvlelem2  38418  hoidmvlelem3  38419  hoidmvlelem5  38421  ovnhoilem1  38423  ovnhoilem2  38424  ovnlecvr2  38432  ovncvr2  38433  hoidifhspf  38440  hspmbllem2  38449  opnvonmbllem2  38455  pfxf  38930  incistruhgr  39171  vtxdgf  39531  c0mgm  39962  c0mhm  39963  c0snmgmhm  39967  funcringcsetcALTV2lem3  40093  funcringcsetclem3ALTV  40116  gsumlsscl  40221  ply1mulgsum  40235  lincfsuppcl  40259  linccl  40260  lincvalsc0  40267  lcoc0  40268  linc0scn0  40269  linc1  40271  lincsum  40275  lincscm  40276  lincscmcl  40278  lcoss  40282  lincext1  40300  el0ldep  40312  lincresunit1  40323  lincresunit3  40327  lmod1zr  40339  fdivmptf  40405  refdivmptf  40406  aacllem  40593
  Copyright terms: Public domain W3C validator