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

Theorem fmptd 5896
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 2791 . 2  |-  ( ph  ->  A. x  e.  A  B  e.  C )
3 fmptd.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43fmpt 5893 . 2  |-  ( A. x  e.  A  B  e.  C  <->  F : A --> C )
52, 4sylib 190 1  |-  ( ph  ->  F : A --> C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653    e. wcel 1726   A.wral 2707    e. cmpt 4269   -->wf 5453
This theorem is referenced by:  fmptco  5904  fliftrel  6033  off  6323  caofinvl  6334  curry1f  6443  curry2f  6445  fnwelem  6464  fdiagfn  7060  resixpfo  7103  pw2f1olem  7215  mapxpen  7276  xpmapenlem  7277  unxpdomlem3  7318  wdom2d  7551  cantnfp1lem1  7637  cantnfp1lem2  7638  cantnfp1lem3  7639  cantnflem1d  7647  cantnflem1  7648  cantnf  7652  fseqenlem1  7910  fseqenlem2  7911  dfac8clem  7918  ac5num  7922  acni2  7932  infpwfien  7948  coftr  8158  fin23lem39  8235  isf34lem2  8258  fin1a2lem12  8296  axcc2lem  8321  axdc2lem  8333  axdc3lem4  8338  pwcfsdom  8463  canthp1lem2  8533  wuncval2  8627  gruf  8691  rpnnen1lem1  10605  monoord2  11359  seqf1o  11369  ccatcl  11748  swrdcl  11771  revcl  11798  revlen  11799  ello1mpt  12320  lo1o12  12332  lo1eq  12367  rlimeq  12368  climmpt2  12372  rlimcld2  12377  climrecl  12382  climge0  12383  o1compt  12386  rlimcn1b  12388  rlimcn2  12389  rlimdiv  12444  rlimsqzlem  12447  isercoll2  12467  caurcvg2  12476  caucvg  12477  sumrblem  12510  summolem2a  12514  fsumf1o  12522  sumss  12523  fsumss  12524  fsumcl2lem  12530  fsumadd  12537  isumclim3  12548  isummulc2  12551  fsummulc2  12572  fsumrelem  12591  climfsum  12604  isumshft  12624  divcnv  12638  supcvg  12640  rpnnen2lem2  12820  crt  13172  eulerthlem1  13175  iserodd  13214  prmreclem2  13290  prmreclem6  13294  1arithlem3  13298  4sqlem11  13328  vdwapf  13345  vdwlem2  13355  vdwlem4  13357  vdwlem6  13359  vdwlem10  13363  ramub1lem2  13400  ramcl  13402  prdsplusg  13686  prdsmulr  13687  prdsvsca  13688  mrcflem  13836  mreacs  13888  acsfn  13889  homaf  14190  prfcl  14305  curf1cl  14330  hofcllem  14360  hofcl  14361  yonedalem3a  14376  yonedalem4c  14379  yonedainv  14383  prdspjmhm  14771  pwsco1mhm  14774  pwsco2mhm  14775  gsumz  14786  gsumwspan  14796  vrmdfval  14806  vrmdf  14808  frmdup1  14814  grpinvf  14854  cycsubgcl  14971  cycsubgss  14972  conjghm  15041  conjnmz  15044  divsghm  15047  galactghm  15111  odf1  15203  dfod2  15205  odf1o2  15212  pgpssslw  15253  sylow2blem1  15259  pj1f  15334  frgpmhm  15402  vrgpf  15405  mulgmhm  15455  mulgghm  15456  iscyggen2  15496  cyggenod  15499  iscyg3  15501  gsumzsplit  15534  gsumsplit2  15536  gsumconst  15537  gsummhm2  15540  gsum2d  15551  prdsgsum  15557  dprdfeq0  15585  dprdlub  15589  dprdz  15593  dprd2dlem1  15604  dprd2da  15605  ablfac1b  15633  ablfac2  15652  rnglghm  15716  rngrghm  15717  gsumdixp  15720  abvtrivd  15933  issrngd  15954  lmodvsghm  16010  lspf  16055  asclf  16401  psrass1lem  16447  psrbas  16448  psrmulcllem  16456  psr1cl  16471  psrlidm  16472  psrridm  16473  psrass1  16474  psrdi  16475  psrdir  16476  psrcom  16477  resspsrmul  16485  subrgpsr  16487  mvridlem  16488  mvrf  16493  mplmon  16531  mplmonmul  16532  mplcoe1  16533  mplcoe3  16534  mplcoe2  16535  mplbas2  16536  psrbagsn  16560  evlslem4  16569  evlslem2  16573  psropprmul  16637  coe1mul2  16667  coe1tmmul2  16673  coe1tmmul  16674  ply1coe  16689  gsumfsum  16771  expmhm  16781  expghm  16782  mulgghm2  16791  isphld  16890  pjff  16944  pptbas  17077  tgrest  17228  resttopon  17230  rest0  17238  restfpw  17248  ordtbaslem  17257  ordtuni  17259  ordtrest  17271  cnpfval  17303  pnrmopn  17412  cncmp  17460  discmp  17466  1stcfb  17513  2ndcomap  17526  dis2ndc  17528  lly1stc  17564  kgencmp  17582  ptpjpre1  17608  ptpjcn  17648  ptcldmpt  17651  ptclsg  17652  dfac14  17655  xkoccn  17656  txcnp  17657  ptcnp  17659  txcnmpt  17661  uptx  17662  ptcn  17664  ptrescn  17676  txlm  17685  xkoptsub  17691  xkoco1cn  17694  xkoco2cn  17695  cnmpt11  17700  xkoinjcn  17724  kqffn  17762  pt1hmeo  17843  fbasrn  17921  trfilss  17926  trfg  17928  rnelfmlem  17989  txflf  18043  flfcnp2  18044  fclscmpi  18066  alexsublem  18080  ptcmplem3  18090  symgtgp  18136  subgntr  18141  opnsubg  18142  clsnsg  18144  tgpconcomp  18147  tsmsfbas  18162  eltsms  18167  haustsms  18170  tsmscls  18172  tsms0  18176  tsmsmhm  18180  tgptsmscls  18184  tsmssplit  18186  tsmsxplem1  18187  tsmsxplem2  18188  ustuqtop0  18275  prdsdsf  18402  prdsxmetlem  18403  imasdsf1olem  18408  prdsbl  18526  stdbdxmet  18550  met1stc  18556  nmf2  18645  nmof  18758  xrge0gsumle  18869  xrge0tsms  18870  metdsf  18883  metdsge  18884  mulc1cncf  18940  cncfmpt2ss  18950  cnmptre  18957  evth  18989  evth2  18990  lebnumlem1  18991  cphnmf  19163  tchcph  19199  cmetcaulem  19246  minveclem1  19330  minveclem3b  19334  ovollb2lem  19389  ovolctb  19391  ovolunlem1a  19397  ovolunlem1  19398  ovoliunlem1  19403  ovoliunlem2  19404  ovoliun  19406  ovolshftlem1  19410  ovolscalem1  19414  ovolicc1  19417  iunmbl  19452  ioombl1lem1  19457  uniioombllem2  19480  uniioombllem3  19482  volsup2  19502  volcn  19503  vitalilem4  19508  vitalilem5  19509  mbfconst  19530  ismbfcn2  19534  mbfeqalem  19537  mbfss  19541  mbfmulc2re  19543  mbfmax  19544  mbfneg  19545  mbfpos  19546  mbfposr  19547  mbfposb  19548  mbfadd  19556  mbfmulc2  19558  mbfsup  19559  mbfinf  19560  mbflimsup  19561  mbflimlem  19562  mbflim  19563  i1f1lem  19584  i1f1  19585  i1fres  19600  itg1climres  19609  mbfi1fseqlem3  19612  mbfi1fseqlem4  19613  mbfi1flimlem  19617  mbfi1flim  19618  mbfmullem2  19619  mbfmul  19621  itg2const2  19636  itg2seq  19637  itg2splitlem  19643  itg2split  19644  itg2monolem1  19645  itg2monolem2  19646  itg2monolem3  19647  itg2mono  19648  itg2i1fseq  19650  itg2i1fseq2  19651  itg2gt0  19655  itg2cnlem1  19656  itg2cnlem2  19657  itg2cn  19658  isibl2  19661  iblss  19699  itgitg1  19703  itgle  19704  itgeqa  19708  itgss3  19709  ibladdlem  19714  itgaddlem1  19717  iblabslem  19722  iblabs  19723  iblabsr  19724  iblmulc2  19725  itgmulc2lem1  19726  bddmulibl  19733  itggt0  19736  itgcn  19737  ellimc2  19769  limcmpt  19775  limcres  19778  limccnp  19783  limccnp2  19784  limcco  19785  perfdvf  19795  dvreslem  19801  dvcnp2  19811  dvaddbr  19829  dvmulbr  19830  dvcjbr  19840  dvexp  19844  dvrec  19846  dvmptres3  19847  dvmptadd  19851  dvmptmul  19852  dvmptres2  19853  dvmptcmul  19855  dvmptcj  19859  dvmptntr  19862  dvmptco  19863  dvcnvlem  19865  dvef  19869  dvferm1  19874  dvferm2  19876  rolle  19879  dvlipcn  19883  dvle  19896  dvivthlem1  19897  dvivth  19899  lhop1lem  19902  lhop1  19903  lhop2  19904  lhop  19905  dvfsumle  19910  dvfsumge  19911  dvmptrecl  19913  dvfsumrlimf  19914  dvfsumlem2  19916  dvfsumlem3  19917  ftc1lem2  19925  ftc1lem6  19930  itgsubstlem  19937  evlslem6  19939  evlslem3  19940  evlslem1  19941  evlsval2  19946  tdeglem1  19986  tdeglem4  19988  coe1mul3  20027  elply2  20120  plyf  20122  elplyd  20126  plypf1  20136  coeeq2  20166  coemullem  20173  coe1termlem  20181  dvply2g  20207  elqaalem2  20242  taylfvallem  20279  taylf  20282  tayl0  20283  taylpfval  20286  taylpf  20287  taylthlem1  20294  taylthlem2  20295  ulmshftlem  20310  ulmshft  20311  ulmcau  20316  ulmss  20318  ulmdvlem1  20321  ulmdvlem3  20323  mtest  20325  mtestbdd  20326  iblulm  20328  itgulm2  20330  psergf  20333  radcnvlem1  20334  dvradcnv  20342  pserulm  20343  psercn2  20344  pserdvlem2  20349  abelthlem4  20355  abelthlem9  20361  pige3  20430  efif1olem4  20452  logtayl  20556  logccv  20559  loglesqr  20647  leibpi  20787  rlimcnp  20809  rlimcnp2  20810  xrlimcnp  20812  efrlim  20813  dfef2  20814  o1cxp  20818  cxp2lim  20820  amgmlem  20833  basellem2  20869  basellem4  20871  basellem7  20874  basellem9  20876  sqff1o  20970  fsumvma  21002  dchrelbasd  21028  lgsfcl2  21091  lgsqrlem2  21131  lgseisenlem1  21138  lgseisenlem3  21140  lgseisenlem4  21141  chpo1ub  21179  dchrisumlema  21187  dchrmusum2  21193  dchrvmasumiflem1  21200  dchrisum0ff  21206  dchrisum0lem1b  21214  dchrisum0lem2a  21216  logsqvma2  21242  pnt2  21312  pnt  21313  abvcxp  21314  padicabv  21329  nbgraf1olem2  21457  vdgrf  21674  vdgrfif  21675  efghgrp  21966  ipblnfi  22362  ubthlem1  22377  minvecolem1  22381  htthlem  22425  hlimadd  22700  chscllem1  23144  hoaddcl  23266  homulcl  23267  brafn  23455  kbop  23461  cnlnadjlem2  23576  strlem3a  23760  hstrlem3a  23768  off2  24059  xppreima2  24065  fmpt3d  24075  xrge0tsmsd  24228  xrge0mulc1cn  24332  esumf1o  24450  esumadd  24453  esumcst  24460  esumpfinval  24470  esumpcvgval  24473  esumcvg  24481  measinb  24580  measdivcst  24584  mbfmco2  24620  sitgclg  24661  dstfrvclim1  24740  lgamgulmlem2  24819  lgamgulmlem6  24823  lgamcvg2  24844  gamcvg  24845  regamcl  24850  relgamcl  24851  erdszelem9  24890  indispcon  24926  cvxpcon  24934  cvmsss2  24966  cvmliftlem6  24982  cvmliftlem8  24984  cvmlift3lem3  25013  divcnvlin  25217  prodfdiv  25229  prodrblem  25260  prodmolem2a  25265  fprodf1o  25277  prodss  25278  fprodss  25279  fprodser  25280  fprodcl2lem  25281  fprodmul  25289  fproddiv  25290  fprodefsum  25303  fprodn0  25308  iprodclim3  25318  iprodefisum  25323  faclimlem2  25368  faclim  25370  faclim2  25372  axlowdimlem15  25900  mblfinlem2  26256  volsupnfl  26263  mbfposadd  26266  itg2addnclem2  26271  itg2gt0cn  26274  ibladdnclem  26275  itgaddnclem1  26277  itgaddnc  26279  iblabsnclem  26282  iblabsnc  26283  iblmulc2nc  26284  itgmulc2nclem1  26285  itgmulc2nclem2  26286  itgmulc2nc  26287  itgabsnc  26288  bddiblnc  26289  itggt0cn  26291  ftc1cnnc  26293  ftc1anclem1  26294  ftc1anclem2  26295  ftc1anclem3  26296  ftc1anclem4  26297  ftc1anclem5  26298  ftc1anclem6  26299  ftc1anclem7  26300  ftc1anclem8  26301  ftc1anc  26302  areacirclem4  26309  comppfsc  26401  upixp  26445  totbndbnd  26512  prdsbnd  26516  cntotbnd  26519  rrnequiv  26558  cmpfiiin  26765  mzpclall  26798  mzpindd  26817  fphpdo  26892  dnnumch3  27136  kelac1  27152  dfac21  27155  pwssplit0  27178  frlmgsum  27223  uvcff  27231  uvcresum  27233  frlmsplit2  27234  frlmup1  27241  pmtrf  27388  psgnunilem5  27408  mamucl  27447  mamulid  27449  mamurid  27450  mamuass  27451  mamudi  27452  mamudir  27453  mamuvs1  27454  mamuvs2  27455  expgrowth  27543  expcnfg  27716  clim1fr1  27717  itgsinexplem1  27738  wlkiswwlk2lem5  28377  frgrancvvdeqlem5  28497  lsatlss  29868  lflnegcl  29947  lshpkrcl  29988  tendoplcl  31652  tendo0cl  31661  tendoicl  31667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pr 4406
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-fv 5465
  Copyright terms: Public domain W3C validator