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

Theorem fmptd 6061
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 2809 . 2  |-  ( ph  ->  A. x  e.  A  B  e.  C )
3 fmptd.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43fmpt 6058 . 2  |-  ( A. x  e.  A  B  e.  C  <->  F : A --> C )
52, 4sylib 201 1  |-  ( ph  ->  F : A --> C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    = wceq 1452    e. wcel 1904   A.wral 2756    |-> cmpt 4454   -->wf 5585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-fv 5597
This theorem is referenced by:  fmpt3d  6062  fmptco  6072  fliftrel  6219  off  6565  caofinvl  6577  curry1f  6909  curry2f  6911  fnwelem  6930  fdiagfn  7533  resixpfo  7578  pw2f1olem  7694  mapxpen  7756  xpmapenlem  7757  unxpdomlem3  7796  fsuppmptdm  7912  fsuppmptif  7931  wdom2d  8113  cantnfp1lem1  8201  cantnfp1lem2  8202  cantnfp1lem3  8203  cantnflem1d  8211  cantnflem1  8212  cantnf  8216  fseqenlem1  8473  fseqenlem2  8474  dfac8clem  8481  ac5num  8485  acni2  8495  infpwfien  8511  coftr  8721  fin23lem39  8798  isf34lem2  8821  fin1a2lem12  8859  axcc2lem  8884  axdc2lem  8896  axdc3lem4  8901  pwcfsdom  9026  canthp1lem2  9096  wuncval2  9190  gruf  9254  rpnnen1lem1  11313  monoord2  12282  seqf1o  12292  ccatcl  12771  swrdcl  12829  revcl  12920  revlen  12921  ello1mpt  13662  lo1o12  13674  lo1eq  13709  rlimeq  13710  climmpt2  13714  climrecl  13724  climge0  13725  o1compt  13728  rlimcn1b  13730  rlimdiv  13786  isercoll2  13809  caurcvg2  13821  caucvg  13822  sumrblem  13854  summolem2a  13858  fsumf1o  13866  sumss  13867  fsumss  13868  fsumcl2lem  13874  fsumadd  13882  isumclim3  13897  isummulc2  13900  fsummulc2  13922  fsumrelem  13944  climfsum  13957  isumshft  13974  divcnv  13988  supcvg  13991  prodfdiv  14029  prodrblem  14060  prodmolem2a  14065  fprodf1o  14077  prodss  14078  fprodss  14079  fprodser  14080  fprodcl2lem  14081  fprodmul  14091  fproddiv  14092  fprodn0  14110  iprodclim3  14130  fprodefsum  14226  rpnnen2lem2  14345  crt  14805  eulerthlem1  14808  iserodd  14864  prmreclem2  14940  prmreclem6  14944  1arithlem3  14948  4sqlem11  14978  vdwapf  15001  vdwlem2  15011  vdwlem4  15013  vdwlem6  15015  vdwlem10  15019  ramub1lem2  15064  ramcl  15066  prmodvdslcmf  15084  prmordvdslcmfOLD  15098  prmordvdslcmsOLDOLD  15100  prmgaplcm  15110  prdsplusg  15434  prdsmulr  15435  prdsvsca  15436  mrcflem  15590  mreacs  15642  acsfn  15643  homaf  16003  funcestrcsetclem3  16105  funcsetcestrclem3  16119  prfcl  16166  curf1cl  16191  hofcllem  16221  hofcl  16222  yonedalem3a  16237  yonedalem4c  16240  yonedainv  16244  prdspjmhm  16692  pwsco1mhm  16695  pwsco2mhm  16696  gsumz  16699  gsumwspan  16708  vrmdfval  16718  vrmdf  16720  frmdup1  16726  grpinvf  16788  cycsubgcl  16921  cycsubgss  16922  conjghm  16991  conjnmz  16994  qusghm  16997  galactghm  17122  symgextf  17136  symgfixf  17155  pmtrf  17174  pmtrdifwrdellem1  17200  psgnunilem5  17213  odf1  17291  dfod2  17293  odf1o2  17300  pgpssslw  17344  sylow2blem1  17350  pj1f  17425  frgpmhm  17493  vrgpf  17496  mulgmhm  17546  mulgghm  17547  iscyggen2  17594  cyggenod  17597  iscyg3  17599  gsummptfsadd  17635  gsumzsplit  17638  gsumsplit2  17640  gsummptfidmsplitres  17642  gsumconst  17645  gsummptshft  17647  gsummhm2  17650  gsummptmhm  17651  gsummptfidminv  17658  gsummptfssub  17660  gsumzunsnd  17666  gsummptf1o  17673  gsummpt1n0  17675  gsum2dlem1  17680  gsum2dlem2  17681  gsum2d  17682  prdsgsum  17688  dprdfeq0  17733  dprdlub  17737  dprdz  17741  dprd2dlem1  17752  dprd2da  17753  ablfac1b  17781  ablfac2  17800  srglmhm  17846  srgrmhm  17847  ringlghm  17910  ringrghm  17911  gsumdixp  17915  abvtrivd  18146  issrngd  18167  lmodvsghm  18227  lspf  18275  pwssplit0  18359  asclf  18638  snifpsrbag  18667  psrass1lem  18678  psrmulcllem  18688  psr1cl  18703  psrlidm  18704  psrridm  18705  psrcom  18710  resspsrmul  18718  subrgpsr  18720  mvrf  18725  mplmon  18764  mplmonmul  18765  mplcoe1  18766  mplcoe5lem  18768  mplcoe5  18769  mplbas2  18771  psrbagsn  18795  evlslem4  18808  evlslem2  18812  evlslem6  18813  evlslem3  18814  evlslem1  18815  evlsval2  18820  psropprmul  18908  coe1mul2  18939  coe1tmmul2  18946  coe1tmmul  18947  ply1coe  18966  ply1coeOLD  18967  gsumsmonply1  18974  gsummoncoe1  18975  gsumfsum  19111  regsumfsum  19112  expmhm  19113  expghm  19144  mulgghm2  19145  evpmodpmf1o  19241  isphld  19298  pjff  19352  frlmgsum  19407  frlmsplit2  19408  frlmphl  19416  uvcff  19426  uvcresum  19428  frlmup1  19433  mamulid  19543  mamurid  19544  scmatf  19631  mdetf  19697  mdetunilem9  19722  mdetuni0  19723  mdetmul  19725  maduf  19743  smadiadetlem3lem1  19768  cpm2mf  19853  m2cpmfo  19857  pmatcollpw1  19877  pmatcollpw3lem  19884  pmatcollpw3fi1lem1  19887  pmatcollpw3fi1lem2  19888  pm2mpcl  19898  mply1topmatcl  19906  mp2pm2mplem2  19908  mp2pm2mp  19912  pm2mpmhmlem2  19920  chfacfisf  19955  chfacfisfcpmat  19956  cpmidpmatlem2  19972  cayhamlem4  19989  pptbas  20100  tgrest  20252  resttopon  20254  rest0  20262  restfpw  20272  ordtbaslem  20281  ordtuni  20283  ordtrest  20295  cnpfval  20327  pnrmopn  20436  cncmp  20484  discmp  20490  1stcfb  20537  2ndcomap  20550  dis2ndc  20552  lly1stc  20588  comppfsc  20624  kgencmp  20637  ptpjpre1  20663  ptpjcn  20703  ptcldmpt  20706  ptclsg  20707  dfac14  20710  xkoccn  20711  txcnp  20712  ptcnp  20714  txcnmpt  20716  uptx  20717  ptcn  20719  ptrescn  20731  txlm  20740  xkoptsub  20746  xkoco1cn  20749  xkoco2cn  20750  cnmpt11  20755  xkoinjcn  20779  kqffn  20817  pt1hmeo  20898  fbasrn  20977  trfilss  20982  trfg  20984  rnelfmlem  21045  txflf  21099  flfcnp2  21100  fclscmpi  21122  alexsublem  21137  ptcmplem3  21147  symgtgp  21194  subgntr  21199  opnsubg  21200  clsnsg  21202  tgpconcomp  21205  tsmsfbas  21220  eltsms  21225  haustsms  21228  tsmscls  21230  tsms0  21234  tsmsmhm  21238  tgptsmscls  21242  tsmssplit  21244  tsmsxplem1  21245  tsmsxplem2  21246  ustuqtop0  21333  prdsdsf  21460  prdsxmetlem  21461  imasdsf1olem  21466  prdsbl  21584  stdbdxmet  21608  met1stc  21614  nmf2  21685  nmofOLD  21820  xrge0gsumle  21929  xrge0tsms  21930  metdsf  21943  metdsge  21944  metdsfOLD  21958  metdsgeOLD  21959  mulc1cncf  22015  cncfmpt2ss  22025  cnmptre  22033  evth  22065  evth2  22066  lebnumlem1  22067  lebnumlem1OLD  22070  cphnmf  22251  tchcph  22289  cmetcaulem  22336  rrxmval  22437  minveclem1  22444  minveclem3b  22448  minveclem3bOLD  22460  ovollb2lem  22519  ovolctb  22521  ovolunlem1a  22527  ovolunlem1  22528  ovoliunlem1  22533  ovoliunlem2  22534  ovoliun  22536  ovolshftlem1  22540  ovolscalem1  22544  ovolicc1  22547  iunmbl  22585  ioombl1lem1  22590  uniioombllem2  22619  uniioombllem2OLD  22620  uniioombllem3  22622  volsup2  22642  volcn  22643  vitalilem4  22648  vitalilem5  22649  mbfconst  22670  ismbfcn2  22674  mbfeqalem  22677  mbfss  22681  mbfmulc2re  22683  mbfmax  22684  mbfneg  22685  mbfpos  22686  mbfposr  22687  mbfposb  22688  mbfadd  22696  mbfmulc2  22698  mbfsup  22699  mbfinf  22700  mbfinfOLD  22701  mbflimsup  22702  mbflimsupOLD  22703  mbflimlem  22704  mbflim  22705  i1f1lem  22726  i1f1  22727  i1fres  22742  itg1climres  22751  mbfi1fseqlem3  22754  mbfi1fseqlem4  22755  mbfi1flimlem  22759  mbfi1flim  22760  mbfmullem2  22761  mbfmul  22763  itg2const2  22778  itg2seq  22779  itg2splitlem  22785  itg2split  22786  itg2monolem1  22787  itg2monolem2  22788  itg2monolem3  22789  itg2mono  22790  itg2i1fseq  22792  itg2i1fseq2  22793  itg2gt0  22797  itg2cnlem1  22798  itg2cnlem2  22799  itg2cn  22800  iblss  22841  itgitg1  22845  itgle  22846  itgeqa  22850  itgss3  22851  ibladdlem  22856  itgaddlem1  22859  iblabslem  22864  iblabs  22865  iblabsr  22866  iblmulc2  22867  itgmulc2lem1  22868  bddmulibl  22875  itggt0  22878  itgcn  22879  ellimc2  22911  limcmpt  22917  limcres  22920  limccnp  22925  limccnp2  22926  limcco  22927  perfdvf  22937  dvreslem  22943  dvcnp2  22953  dvaddbr  22971  dvmulbr  22972  dvcjbr  22982  dvexp  22986  dvrec  22988  dvmptres3  22989  dvmptadd  22993  dvmptmul  22994  dvmptres2  22995  dvmptcmul  22997  dvmptcj  23001  dvmptntr  23004  dvmptco  23005  dvcnvlem  23007  dvef  23011  dvferm1  23016  dvferm2  23018  rolle  23021  dvlipcn  23025  dvle  23038  dvivthlem1  23039  dvivth  23041  lhop1lem  23044  lhop1  23045  lhop2  23046  lhop  23047  dvfsumle  23052  dvfsumge  23053  dvmptrecl  23055  dvfsumrlimf  23056  dvfsumlem2  23058  dvfsumlem3  23059  ftc1lem2  23067  ftc1lem6  23072  itgsubstlem  23079  tdeglem1  23086  tdeglem4  23088  coe1mul3  23127  elply2  23229  plyf  23231  elplyd  23235  plypf1  23245  coeeq2  23275  coemullem  23283  coe1termlem  23291  dvply2g  23317  elqaalem2  23352  elqaalem2OLD  23355  taylfvallem  23392  taylf  23395  tayl0  23396  taylpfval  23399  taylpf  23400  taylthlem1  23407  taylthlem2  23408  ulmshftlem  23423  ulmshft  23424  ulmcau  23429  ulmss  23431  ulmdvlem1  23434  ulmdvlem3  23436  mtest  23438  mtestbdd  23439  itgulm2  23443  psergf  23446  radcnvlem1  23447  dvradcnv  23455  pserulm  23456  psercn2  23457  pserdvlem2  23462  abelthlem4  23468  abelthlem9  23474  pige3  23551  efif1olem4  23573  logtayl  23684  logccv  23687  loglesqrt  23777  logbf  23805  leibpi  23947  rlimcnp  23970  rlimcnp2  23971  xrlimcnp  23973  efrlim  23974  dfef2  23975  o1cxp  23979  cxp2lim  23981  amgmlem  23994  lgamgulmlem2  24034  lgamgulmlem6  24038  lgamcvg2  24059  gamcvg  24060  regamcl  24065  relgamcl  24066  basellem2  24087  basellem4  24089  basellem7  24092  basellem9  24094  sqff1o  24188  fsumvma  24220  dchrelbasd  24246  lgsfcl2  24309  lgsqrlem2  24349  lgseisenlem1  24356  lgseisenlem3  24358  lgseisenlem4  24359  chpo1ub  24397  dchrmusum2  24411  dchrvmasumiflem1  24418  dchrisum0ff  24424  dchrisum0lem1b  24432  dchrisum0lem2a  24434  logsqvma2  24460  pnt2  24530  pnt  24531  abvcxp  24532  padicabv  24547  lmif  24906  axlowdimlem15  25065  nbgraf1olem2  25249  wlkiswwlk2lem5  25502  wlknwwlknfun  25517  wlkiswwlkfun  25524  wwlkextfun  25536  clwlkisclwwlklem2a  25592  clwwlkf  25601  clwlkfclwwlk  25651  vdgrf  25705  vdgrfif  25706  frgrancvvdeqlem5  25841  numclwlk1lem2f  25899  numclwlk2lem2f  25910  efghgrpOLD  26182  ipblnfi  26578  ubthlem1  26593  minvecolem1  26597  htthlem  26651  hlimadd  26927  chscllem1  27371  hoaddcl  27492  homulcl  27493  brafn  27681  kbop  27687  cnlnadjlem2  27802  strlem3a  27986  hstrlem3a  27994  off2  28318  xppreima2  28325  fpwrelmap  28393  gsummpt2d  28618  gsumvsca1  28619  gsumvsca2  28620  xrge0tsmsd  28622  ordtrestNEW  28801  xrge0mulc1cn  28821  esumf1o  28945  esumadd  28952  esumcst  28958  esumpfinval  28970  esumpcvgval  28973  esumcvg  28981  esumsup  28984  measinb  29117  measdivcst  29121  mbfmco2  29160  sitgclg  29248  eulerpartlems  29266  dstfrvclim1  29383  gsumncl  29496  gsumnunsn  29497  erdszelem9  29994  indispcon  30029  cvxpcon  30037  cvmsss2  30069  cvmliftlem6  30085  cvmliftlem8  30087  cvmlift3lem3  30116  mrsubcv  30220  mrsubff  30222  mrsubrn  30223  mrsubccat  30228  elmrsubrn  30230  msubrn  30239  msubff  30240  mvhf  30268  divcnvlin  30438  iprodefisum  30448  faclimlem2  30451  faclim  30453  faclim2  30455  finixpnum  31994  ptrest  32003  poimirlem17  32021  poimirlem20  32024  poimirlem24  32028  poimirlem30  32034  broucube  32038  mblfinlem2  32042  volsupnfl  32049  mbfposadd  32052  itg2addnclem2  32058  itg2gt0cn  32061  ibladdnclem  32062  itgaddnclem1  32064  itgaddnc  32066  iblabsnclem  32069  iblabsnc  32070  iblmulc2nc  32071  itgmulc2nclem1  32072  itgmulc2nclem2  32073  itgmulc2nc  32074  itgabsnc  32075  bddiblnc  32076  itggt0cn  32078  ftc1cnnc  32080  ftc1anclem1  32081  ftc1anclem2  32082  ftc1anclem3  32083  ftc1anclem4  32084  ftc1anclem5  32085  ftc1anclem6  32086  ftc1anclem7  32087  ftc1anclem8  32088  ftc1anc  32089  areacirclem4  32099  upixp  32120  totbndbnd  32185  prdsbnd  32189  cntotbnd  32192  rrnequiv  32231  lsatlss  32633  lflnegcl  32712  lshpkrcl  32753  tendoplcl  34419  tendo0cl  34428  tendoicl  34434  cmpfiiin  35610  mzpclall  35640  mzpindd  35659  fphpdo  35731  dnnumch3  35976  kelac1  35992  dfac21  35995  itgpowd  36170  expgrowth  36754  binomcxplemradcnv  36771  binomcxplemcvg  36773  binomcxplemnotnn0  36775  rnmptc  37510  mptelpm  37514  projf1o  37545  mapss2  37557  expcnfg  37768  clim1fr1  37776  mullimc  37793  ellimcabssub0  37794  mullimcf  37800  constlimc  37801  idlimc  37803  sumnnodd  37807  neglimc  37825  addlimc  37826  0ellimcdiv  37827  cncfmptssg  37844  cncfshift  37848  cncfcompt  37857  icccncfext  37862  cncfiooiccre  37870  cxpcncf2  37875  dvsinax  37880  fperdvper  37887  dvmptresicc  37888  dvcosax  37895  ioodvbdlimc1lem1  37900  ioodvbdlimc1lem2  37901  ioodvbdlimc1lem1OLD  37902  ioodvbdlimc1lem2OLD  37903  ioodvbdlimc2lem  37905  ioodvbdlimc2lemOLD  37906  dvnmptdivc  37910  dvnxpaek  37914  dvnprodlem1  37918  dvnprodlem2  37919  dvnprodlem3  37920  itgsinexplem1  37927  iblsplit  37940  itgcoscmulx  37943  itgiccshift  37954  itgperiod  37955  itgsbtaddcnst  37956  dirkerf  38071  dirkeritg  38076  dirkercncflem2  38078  fourierdlem4  38085  fourierdlem5  38086  fourierdlem9  38090  fourierdlem14  38095  fourierdlem16  38097  fourierdlem17  38098  fourierdlem18  38099  fourierdlem21  38102  fourierdlem22  38103  fourierdlem37  38119  fourierdlem50  38132  fourierdlem51  38133  fourierdlem53  38135  fourierdlem55  38137  fourierdlem57  38139  fourierdlem58  38140  fourierdlem59  38141  fourierdlem60  38142  fourierdlem61  38143  fourierdlem67  38149  fourierdlem68  38150  fourierdlem72  38154  fourierdlem73  38155  fourierdlem74  38156  fourierdlem75  38157  fourierdlem76  38158  fourierdlem78  38160  fourierdlem80  38162  fourierdlem81  38163  fourierdlem83  38165  fourierdlem84  38166  fourierdlem88  38170  fourierdlem92  38174  fourierdlem93  38175  fourierdlem97  38179  fourierdlem101  38183  fourierdlem103  38185  fourierdlem104  38186  fourierdlem111  38193  sqwvfoura  38204  elaa2lem  38209  elaa2lemOLD  38210  etransclem1  38212  etransclem8  38219  etransclem20  38231  etransclem33  38244  etransclem35  38246  etransclem39  38250  rrxtopnfi  38267  sge0tsms  38336  sge0snmpt  38339  sge0fsummpt  38346  sge0pr  38350  sge0lessmpt  38355  sge0iunmptlemfi  38369  sge0iunmptlemre  38371  sge0iunmpt  38374  sge0rpcpnf  38377  sge0isum  38383  nnfoctbdjlem  38409  psmeasure  38425  voliunsge0lem  38426  omeiunltfirp  38459  carageniuncllem2  38462  caratheodorylem1  38466  caratheodorylem2  38467  isomenndlem  38470  hoicvr  38488  hoicvrrex  38496  ovnsupge0  38497  ovnlecvr  38498  ovnf  38503  ovn0lem  38505  ovnsubaddlem1  38510  ovnsubadd  38512  hsphoif  38516  sge0hsphoire  38529  hoidmv1lelem1  38531  hoidmv1lelem2  38532  hoidmv1lelem3  38533  hoidmv1le  38534  hoidmvlelem1  38535  hoidmvlelem2  38536  hoidmvlelem3  38537  hoidmvlelem5  38539  ovnhoilem1  38541  ovnhoilem2  38542  ovnlecvr2  38550  ovncvr2  38551  hoidifhspf  38558  hspmbllem2  38567  opnvonmbllem2  38573  ovnsubadd2lem  38585  ovolval4lem1  38589  ovolval4lem2  38590  ovolval5lem2  38593  ovnovollem1  38596  ovnovollem2  38597  pfxf  39077  incistruhgr  39325  vtxdgf  39696  crctcsh1wlkn0  39999  c0mgm  40417  c0mhm  40418  c0snmgmhm  40422  funcringcsetcALTV2lem3  40548  funcringcsetclem3ALTV  40571  gsumlsscl  40676  ply1mulgsum  40690  lincfsuppcl  40714  linccl  40715  lincvalsc0  40722  lcoc0  40723  linc0scn0  40724  linc1  40726  lincsum  40730  lincscm  40731  lincscmcl  40733  lcoss  40737  lincext1  40755  el0ldep  40767  lincresunit1  40778  lincresunit3  40782  lmod1zr  40794  fdivmptf  40860  refdivmptf  40861  aacllem  41046
  Copyright terms: Public domain W3C validator