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

Theorem fmptd 6043
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 2878 . 2  |-  ( ph  ->  A. x  e.  A  B  e.  C )
3 fmptd.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43fmpt 6040 . 2  |-  ( A. x  e.  A  B  e.  C  <->  F : A --> C )
52, 4sylib 196 1  |-  ( ph  ->  F : A --> C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379    e. wcel 1767   A.wral 2814    |-> cmpt 4505   -->wf 5582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-fv 5594
This theorem is referenced by:  fmptco  6052  fliftrel  6192  off  6536  caofinvl  6549  curry1f  6874  curry2f  6876  fnwelem  6895  fdiagfn  7459  resixpfo  7504  pw2f1olem  7618  mapxpen  7680  xpmapenlem  7681  unxpdomlem3  7723  fsuppmptdm  7836  fsuppmptif  7855  wdom2d  8002  cantnfp1lem1  8093  cantnfp1lem2  8094  cantnfp1lem3  8095  cantnflem1d  8103  cantnflem1  8104  cantnf  8108  cantnfp1lem1OLD  8119  cantnfp1lem2OLD  8120  cantnfp1lem3OLD  8121  cantnflem1dOLD  8126  cantnflem1OLD  8127  cantnfOLD  8130  fseqenlem1  8401  fseqenlem2  8402  dfac8clem  8409  ac5num  8413  acni2  8423  infpwfien  8439  coftr  8649  fin23lem39  8726  isf34lem2  8749  fin1a2lem12  8787  axcc2lem  8812  axdc2lem  8824  axdc3lem4  8829  pwcfsdom  8954  canthp1lem2  9027  wuncval2  9121  gruf  9185  rpnnen1lem1  11204  monoord2  12101  seqf1o  12111  ccatcl  12552  swrdcl  12603  revcl  12692  revlen  12693  ello1mpt  13300  lo1o12  13312  lo1eq  13347  rlimeq  13348  climmpt2  13352  rlimcld2  13357  climrecl  13362  climge0  13363  o1compt  13366  rlimcn1b  13368  rlimcn2  13369  rlimdiv  13424  rlimsqzlem  13427  isercoll2  13447  caurcvg2  13456  caucvg  13457  sumrblem  13489  summolem2a  13493  fsumf1o  13501  sumss  13502  fsumss  13503  fsumcl2lem  13509  fsumadd  13517  isumclim3  13530  isummulc2  13533  fsummulc2  13555  fsumrelem  13577  climfsum  13590  isumshft  13607  divcnv  13621  supcvg  13623  rpnnen2lem2  13803  crt  14160  eulerthlem1  14163  iserodd  14211  prmreclem2  14287  prmreclem6  14291  1arithlem3  14295  4sqlem11  14325  vdwapf  14342  vdwlem2  14352  vdwlem4  14354  vdwlem6  14356  vdwlem10  14360  ramub1lem2  14397  ramcl  14399  prdsplusg  14706  prdsmulr  14707  prdsvsca  14708  mrcflem  14854  mreacs  14906  acsfn  14907  homaf  15208  prfcl  15323  curf1cl  15348  hofcllem  15378  hofcl  15379  yonedalem3a  15394  yonedalem4c  15397  yonedainv  15401  prdspjmhm  15805  pwsco1mhm  15808  pwsco2mhm  15809  gsumz  15821  gsumwspan  15834  vrmdfval  15844  vrmdf  15846  frmdup1  15852  grpinvf  15892  cycsubgcl  16019  cycsubgss  16020  conjghm  16089  conjnmz  16092  divsghm  16095  galactghm  16220  symgextf  16234  symgfixf  16254  pmtrf  16273  psgnunilem5  16312  odf1  16377  dfod2  16379  odf1o2  16386  pgpssslw  16427  sylow2blem1  16433  pj1f  16508  frgpmhm  16576  vrgpf  16579  mulgmhm  16629  mulgghm  16630  iscyggen2  16672  cyggenod  16675  iscyg3  16677  gsummptfsadd  16728  gsummptfsaddOLD  16729  gsumzsplit  16732  gsumzsplitOLD  16733  gsumsplit2  16736  gsumsplit2OLD  16737  gsummptfidmsplitres  16739  gsumconst  16742  gsummptshft  16744  gsummhm2  16749  gsummhm2OLD  16750  gsummptmhm  16751  gsummptfidminv  16760  gsummptfssub  16764  gsumzunsnd  16770  gsummptf1o  16778  gsummpt1n0  16780  gsum2dlem1  16785  gsum2dlem2  16786  gsum2d  16787  gsum2dOLD  16788  prdsgsum  16795  prdsgsumOLD  16796  dprdfeq0  16849  dprdfeq0OLD  16856  dprdlub  16860  dprdz  16864  dprd2dlem1  16877  dprd2da  16878  ablfac1b  16908  ablfac2  16927  srglmhm  16971  srgrmhm  16972  rnglghm  17031  rngrghm  17032  gsumdixpOLD  17038  gsumdixp  17039  abvtrivd  17269  issrngd  17290  lmodvsghm  17351  lspf  17400  pwssplit0  17484  asclf  17754  snifpsrbag  17783  psrass1lem  17797  psrbasOLD  17799  psrmulcllem  17808  psr1cl  17823  psrlidm  17824  psrlidmOLD  17825  psrridm  17826  psrridmOLD  17827  psrdi  17829  psrdir  17830  psrcom  17832  resspsrmul  17840  subrgpsr  17842  mvridlemOLD  17843  mvrf  17848  mplmon  17893  mplmonmul  17894  mplcoe1  17895  mplcoe3OLD  17897  mplcoe5lem  17898  mplcoe5  17899  mplcoe2OLD  17901  mplbas2  17902  mplbas2OLD  17903  psrbagsn  17928  evlslem4OLD  17941  evlslem4  17942  evlslem2  17948  evlslem6  17949  evlslem6OLD  17950  evlslem3  17951  evlslem1  17952  evlsval2  17957  psropprmul  18047  coe1mul2  18078  coe1tmmul2  18085  coe1tmmul  18086  ply1coe  18105  ply1coeOLD  18106  gsumsmonply1  18113  gsummoncoe1  18114  gsumfsum  18249  expmhm  18250  expghm  18293  expghmOLD  18294  mulgghm2  18295  mulgghm2OLD  18298  evpmodpmf1o  18396  isphld  18453  pjff  18507  frlmgsumOLD  18565  frlmgsum  18566  frlmsplit2  18567  frlmphl  18576  uvcff  18586  uvcresum  18588  frlmup1  18596  mamulid  18707  mamurid  18708  scmatf  18795  mdetf  18861  mdetunilem9  18886  mdetuni0  18887  mdetmul  18889  maduf  18907  cpm2mf  19017  m2cpmfo  19021  pmatcollpw1  19041  pmatcollpw3lem  19048  pmatcollpw3fi1lem1  19051  pmatcollpw3fi1lem2  19052  pm2mpcl  19062  mply1topmatcl  19070  mp2pm2mplem2  19072  mp2pm2mp  19076  pm2mpmhmlem2  19084  chfacfisf  19119  chfacfisfcpmat  19120  cpmidpmatlem2  19136  cayhamlem4  19153  pptbas  19272  tgrest  19423  resttopon  19425  rest0  19433  restfpw  19443  ordtbaslem  19452  ordtuni  19454  ordtrest  19466  cnpfval  19498  pnrmopn  19607  cncmp  19655  discmp  19661  1stcfb  19709  2ndcomap  19722  dis2ndc  19724  lly1stc  19760  kgencmp  19778  ptpjpre1  19804  ptpjcn  19844  ptcldmpt  19847  ptclsg  19848  dfac14  19851  xkoccn  19852  txcnp  19853  ptcnp  19855  txcnmpt  19857  uptx  19858  ptcn  19860  ptrescn  19872  txlm  19881  xkoptsub  19887  xkoco1cn  19890  xkoco2cn  19891  cnmpt11  19896  xkoinjcn  19920  kqffn  19958  pt1hmeo  20039  fbasrn  20117  trfilss  20122  trfg  20124  rnelfmlem  20185  txflf  20239  flfcnp2  20240  fclscmpi  20262  alexsublem  20276  ptcmplem3  20286  symgtgp  20332  subgntr  20337  opnsubg  20338  clsnsg  20340  tgpconcomp  20343  tsmsfbas  20358  eltsms  20363  haustsms  20366  tsmscls  20368  tsms0  20375  tsmsmhm  20380  tgptsmscls  20384  tsmssplit  20386  tsmsxplem1  20387  tsmsxplem2  20388  ustuqtop0  20475  prdsdsf  20602  prdsxmetlem  20603  imasdsf1olem  20608  prdsbl  20726  stdbdxmet  20750  met1stc  20756  nmf2  20845  nmof  20958  xrge0gsumle  21070  xrge0tsms  21071  metdsf  21084  metdsge  21085  mulc1cncf  21141  cncfmpt2ss  21151  cnmptre  21159  evth  21191  evth2  21192  lebnumlem1  21193  cphnmf  21374  tchcph  21412  cmetcaulem  21459  rrxmval  21564  minveclem1  21571  minveclem3b  21575  ovollb2lem  21631  ovolctb  21633  ovolunlem1a  21639  ovolunlem1  21640  ovoliunlem1  21645  ovoliunlem2  21646  ovoliun  21648  ovolshftlem1  21652  ovolscalem1  21656  ovolicc1  21659  iunmbl  21695  ioombl1lem1  21700  uniioombllem2  21724  uniioombllem3  21726  volsup2  21746  volcn  21747  vitalilem4  21752  vitalilem5  21753  mbfconst  21774  ismbfcn2  21778  mbfeqalem  21781  mbfss  21785  mbfmulc2re  21787  mbfmax  21788  mbfneg  21789  mbfpos  21790  mbfposr  21791  mbfposb  21792  mbfadd  21800  mbfmulc2  21802  mbfsup  21803  mbfinf  21804  mbflimsup  21805  mbflimlem  21806  mbflim  21807  i1f1lem  21828  i1f1  21829  i1fres  21844  itg1climres  21853  mbfi1fseqlem3  21856  mbfi1fseqlem4  21857  mbfi1flimlem  21861  mbfi1flim  21862  mbfmullem2  21863  mbfmul  21865  itg2const2  21880  itg2seq  21881  itg2splitlem  21887  itg2split  21888  itg2monolem1  21889  itg2monolem2  21890  itg2monolem3  21891  itg2mono  21892  itg2i1fseq  21894  itg2i1fseq2  21895  itg2gt0  21899  itg2cnlem1  21900  itg2cnlem2  21901  itg2cn  21902  isibl2  21905  iblss  21943  itgitg1  21947  itgle  21948  itgeqa  21952  itgss3  21953  ibladdlem  21958  itgaddlem1  21961  iblabslem  21966  iblabs  21967  iblabsr  21968  iblmulc2  21969  itgmulc2lem1  21970  bddmulibl  21977  itggt0  21980  itgcn  21981  ellimc2  22013  limcmpt  22019  limcres  22022  limccnp  22027  limccnp2  22028  limcco  22029  perfdvf  22039  dvreslem  22045  dvcnp2  22055  dvaddbr  22073  dvmulbr  22074  dvcjbr  22084  dvexp  22088  dvrec  22090  dvmptres3  22091  dvmptadd  22095  dvmptmul  22096  dvmptres2  22097  dvmptcmul  22099  dvmptcj  22103  dvmptntr  22106  dvmptco  22107  dvcnvlem  22109  dvef  22113  dvferm1  22118  dvferm2  22120  rolle  22123  dvlipcn  22127  dvle  22140  dvivthlem1  22141  dvivth  22143  lhop1lem  22146  lhop1  22147  lhop2  22148  lhop  22149  dvfsumle  22154  dvfsumge  22155  dvmptrecl  22157  dvfsumrlimf  22158  dvfsumlem2  22160  dvfsumlem3  22161  ftc1lem2  22169  ftc1lem6  22174  itgsubstlem  22181  tdeglem1  22188  tdeglem4  22190  coe1mul3  22232  elply2  22325  plyf  22327  elplyd  22331  plypf1  22341  coeeq2  22371  coemullem  22378  coe1termlem  22386  dvply2g  22412  elqaalem2  22447  taylfvallem  22484  taylf  22487  tayl0  22488  taylpfval  22491  taylpf  22492  taylthlem1  22499  taylthlem2  22500  ulmshftlem  22515  ulmshft  22516  ulmcau  22521  ulmss  22523  ulmdvlem1  22526  ulmdvlem3  22528  mtest  22530  mtestbdd  22531  iblulm  22533  itgulm2  22535  psergf  22538  radcnvlem1  22539  dvradcnv  22547  pserulm  22548  psercn2  22549  pserdvlem2  22554  abelthlem4  22560  abelthlem9  22566  pige3  22640  efif1olem4  22662  logtayl  22766  logccv  22769  loglesqrt  22857  leibpi  22998  rlimcnp  23020  rlimcnp2  23021  xrlimcnp  23023  efrlim  23024  dfef2  23025  o1cxp  23029  cxp2lim  23031  amgmlem  23044  basellem2  23080  basellem4  23082  basellem7  23085  basellem9  23087  sqff1o  23181  fsumvma  23213  dchrelbasd  23239  lgsfcl2  23302  lgsqrlem2  23342  lgseisenlem1  23349  lgseisenlem3  23351  lgseisenlem4  23352  chpo1ub  23390  dchrisumlema  23398  dchrmusum2  23404  dchrvmasumiflem1  23411  dchrisum0ff  23417  dchrisum0lem1b  23425  dchrisum0lem2a  23427  logsqvma2  23453  pnt2  23523  pnt  23524  abvcxp  23525  padicabv  23540  lmif  23825  axlowdimlem15  23932  nbgraf1olem2  24115  wlkiswwlk2lem5  24368  wlknwwlknfun  24383  wlkiswwlkfun  24390  wwlkextfun  24402  clwlkisclwwlklem2a  24458  clwwlkf  24467  clwlkfclwwlk  24517  vdgrf  24571  vdgrfif  24572  frgrancvvdeqlem5  24708  numclwlk1lem2f  24766  numclwlk2lem2f  24777  efghgrp  25048  ipblnfi  25444  ubthlem1  25459  minvecolem1  25463  htthlem  25507  hlimadd  25783  chscllem1  26228  hoaddcl  26350  homulcl  26351  brafn  26539  kbop  26545  cnlnadjlem2  26660  strlem3a  26844  hstrlem3a  26852  off2  27151  xppreima2  27157  fmpt3d  27165  fpwrelmap  27225  regsumfsum  27432  gsumvsca1  27433  gsumvsca2  27434  xrge0tsmsd  27435  ordtrestNEW  27536  xrge0mulc1cn  27556  esumf1o  27698  esumadd  27701  esumcst  27708  esumpfinval  27718  esumpcvgval  27721  esumcvg  27729  measinb  27829  measdivcst  27833  mbfmco2  27873  sitgclg  27921  eulerpartlems  27936  dstfrvclim1  28053  gsumncl  28129  gsumnunsn  28130  signstf  28160  lgamgulmlem2  28209  lgamgulmlem6  28213  lgamcvg2  28234  gamcvg  28235  regamcl  28240  relgamcl  28241  erdszelem9  28280  indispcon  28316  cvxpcon  28324  cvmsss2  28356  cvmliftlem6  28372  cvmliftlem8  28374  cvmlift3lem3  28403  divcnvlin  28592  prodfdiv  28604  prodrblem  28635  prodmolem2a  28640  fprodf1o  28652  prodss  28653  fprodss  28654  fprodser  28655  fprodcl2lem  28656  fprodmul  28664  fproddiv  28665  fprodefsum  28678  fprodn0  28683  iprodclim3  28693  iprodefisum  28698  faclimlem2  28743  faclim  28745  faclim2  28747  finixpnum  29612  ptrest  29623  mblfinlem2  29627  volsupnfl  29634  mbfposadd  29637  itg2addnclem2  29642  itg2gt0cn  29645  ibladdnclem  29646  itgaddnclem1  29648  itgaddnc  29650  iblabsnclem  29653  iblabsnc  29654  iblmulc2nc  29655  itgmulc2nclem1  29656  itgmulc2nclem2  29657  itgmulc2nc  29658  itgabsnc  29659  bddiblnc  29660  itggt0cn  29662  ftc1cnnc  29664  ftc1anclem1  29665  ftc1anclem2  29666  ftc1anclem3  29667  ftc1anclem4  29668  ftc1anclem5  29669  ftc1anclem6  29670  ftc1anclem7  29671  ftc1anclem8  29672  ftc1anc  29673  areacirclem4  29685  comppfsc  29777  upixp  29821  totbndbnd  29886  prdsbnd  29890  cntotbnd  29893  rrnequiv  29932  cmpfiiin  30231  mzpclall  30261  mzpindd  30280  fphpdo  30353  dnnumch3  30597  kelac1  30613  dfac21  30616  itgpowd  30787  expgrowth  30840  rnmptc  31027  expcnfg  31142  clim1fr1  31143  mullimc  31158  ellimcabssub0  31159  mullimcf  31165  constlimc  31166  idlimc  31168  sumnnodd  31172  neglimc  31189  addlimc  31190  0ellimcdiv  31191  cncfshift  31212  cncfcompt  31221  cncfiooiccre  31234  dvsinax  31241  fperdvper  31248  dvmptresicc  31249  ioodvbdlimc1lem1  31261  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  itgsinexplem1  31271  itgcoscmulx  31287  itgiccshift  31298  itgperiod  31299  dirkerf  31397  dirkeritg  31402  dirkercncflem2  31404  dirkercncflem4  31406  fourierdlem4  31411  fourierdlem5  31412  fourierdlem9  31416  fourierdlem14  31421  fourierdlem16  31423  fourierdlem17  31424  fourierdlem18  31425  fourierdlem21  31428  fourierdlem22  31429  fourierdlem37  31444  fourierdlem45  31452  fourierdlem50  31457  fourierdlem51  31458  fourierdlem53  31460  fourierdlem55  31462  fourierdlem58  31465  fourierdlem59  31466  fourierdlem60  31467  fourierdlem61  31468  fourierdlem67  31474  fourierdlem68  31475  fourierdlem72  31479  fourierdlem73  31480  fourierdlem74  31481  fourierdlem75  31482  fourierdlem76  31483  fourierdlem78  31485  fourierdlem80  31487  fourierdlem81  31488  fourierdlem83  31490  fourierdlem84  31491  fourierdlem88  31495  fourierdlem92  31499  fourierdlem97  31504  fourierdlem101  31508  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  sqwvfoura  31529  gsumlsscl  32049  ply1mulgsum  32063  lincfsuppcl  32087  linccl  32088  lincvalsc0  32095  lcoc0  32096  linc0scn0  32097  linc1  32099  lincsum  32103  lincscm  32104  lincscmcl  32106  lcoss  32110  lincext1  32128  el0ldep  32140  lincresunit1  32151  lincresunit3  32155  lmod1zr  32175  lsatlss  33793  lflnegcl  33872  lshpkrcl  33913  tendoplcl  35577  tendo0cl  35586  tendoicl  35592
  Copyright terms: Public domain W3C validator