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

Theorem fmptd 6040
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 2857 . 2  |-  ( ph  ->  A. x  e.  A  B  e.  C )
3 fmptd.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43fmpt 6037 . 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 1383    e. wcel 1804   A.wral 2793    |-> cmpt 4495   -->wf 5574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-fv 5586
This theorem is referenced by:  fmptco  6049  fliftrel  6191  off  6539  caofinvl  6552  curry1f  6879  curry2f  6881  fnwelem  6900  fdiagfn  7464  resixpfo  7509  pw2f1olem  7623  mapxpen  7685  xpmapenlem  7686  unxpdomlem3  7728  fsuppmptdm  7842  fsuppmptif  7861  wdom2d  8009  cantnfp1lem1  8100  cantnfp1lem2  8101  cantnfp1lem3  8102  cantnflem1d  8110  cantnflem1  8111  cantnf  8115  cantnfp1lem1OLD  8126  cantnfp1lem2OLD  8127  cantnfp1lem3OLD  8128  cantnflem1dOLD  8133  cantnflem1OLD  8134  cantnfOLD  8137  fseqenlem1  8408  fseqenlem2  8409  dfac8clem  8416  ac5num  8420  acni2  8430  infpwfien  8446  coftr  8656  fin23lem39  8733  isf34lem2  8756  fin1a2lem12  8794  axcc2lem  8819  axdc2lem  8831  axdc3lem4  8836  pwcfsdom  8961  canthp1lem2  9034  wuncval2  9128  gruf  9192  rpnnen1lem1  11219  monoord2  12120  seqf1o  12130  ccatcl  12575  swrdcl  12628  revcl  12717  revlen  12718  ello1mpt  13326  lo1o12  13338  lo1eq  13373  rlimeq  13374  climmpt2  13378  climrecl  13388  climge0  13389  o1compt  13392  rlimcn1b  13394  rlimdiv  13450  isercoll2  13473  caurcvg2  13482  caucvg  13483  sumrblem  13515  summolem2a  13519  fsumf1o  13527  sumss  13528  fsumss  13529  fsumcl2lem  13535  fsumadd  13543  isumclim3  13556  isummulc2  13559  fsummulc2  13581  fsumrelem  13603  climfsum  13616  isumshft  13633  divcnv  13647  supcvg  13649  prodfdiv  13687  prodrblem  13718  prodmolem2a  13723  fprodf1o  13735  prodss  13736  fprodss  13737  fprodser  13738  fprodcl2lem  13739  fprodmul  13747  fproddiv  13748  fprodn0  13765  iprodclim3  13775  fprodefsum  13812  rpnnen2lem2  13931  crt  14290  eulerthlem1  14293  iserodd  14341  prmreclem2  14417  prmreclem6  14421  1arithlem3  14425  4sqlem11  14455  vdwapf  14472  vdwlem2  14482  vdwlem4  14484  vdwlem6  14486  vdwlem10  14490  ramub1lem2  14527  ramcl  14529  prdsplusg  14837  prdsmulr  14838  prdsvsca  14839  mrcflem  14985  mreacs  15037  acsfn  15038  homaf  15336  prfcl  15451  curf1cl  15476  hofcllem  15506  hofcl  15507  yonedalem3a  15522  yonedalem4c  15525  yonedainv  15529  prdspjmhm  15977  pwsco1mhm  15980  pwsco2mhm  15981  gsumz  15984  gsumwspan  15993  vrmdfval  16003  vrmdf  16005  frmdup1  16011  grpinvf  16073  cycsubgcl  16206  cycsubgss  16207  conjghm  16276  conjnmz  16279  qusghm  16282  galactghm  16407  symgextf  16421  symgfixf  16440  pmtrf  16459  pmtrdifwrdellem1  16485  psgnunilem5  16498  odf1  16563  dfod2  16565  odf1o2  16572  pgpssslw  16613  sylow2blem1  16619  pj1f  16694  frgpmhm  16762  vrgpf  16765  mulgmhm  16815  mulgghm  16816  iscyggen2  16863  cyggenod  16866  iscyg3  16868  gsummptfsadd  16919  gsummptfsaddOLD  16920  gsumzsplit  16923  gsumzsplitOLD  16924  gsumsplit2  16927  gsumsplit2OLD  16928  gsummptfidmsplitres  16930  gsumconst  16933  gsummptshft  16935  gsummhm2  16940  gsummhm2OLD  16941  gsummptmhm  16942  gsummptfidminv  16951  gsummptfssub  16955  gsumzunsnd  16961  gsummptf1o  16969  gsummpt1n0  16971  gsum2dlem1  16976  gsum2dlem2  16977  gsum2d  16978  gsum2dOLD  16979  prdsgsum  16986  prdsgsumOLD  16987  dprdfeq0  17041  dprdfeq0OLD  17048  dprdlub  17052  dprdz  17056  dprd2dlem1  17069  dprd2da  17070  ablfac1b  17100  ablfac2  17119  srglmhm  17165  srgrmhm  17166  ringlghm  17229  ringrghm  17230  gsumdixpOLD  17236  gsumdixp  17237  abvtrivd  17468  issrngd  17489  lmodvsghm  17550  lspf  17599  pwssplit0  17683  asclf  17965  snifpsrbag  17994  psrass1lem  18008  psrbasOLD  18010  psrmulcllem  18019  psr1cl  18034  psrlidm  18035  psrlidmOLD  18036  psrridm  18037  psrridmOLD  18038  psrcom  18043  resspsrmul  18051  subrgpsr  18053  mvridlemOLD  18054  mvrf  18059  mplmon  18104  mplmonmul  18105  mplcoe1  18106  mplcoe3OLD  18108  mplcoe5lem  18109  mplcoe5  18110  mplcoe2OLD  18112  mplbas2  18113  mplbas2OLD  18114  psrbagsn  18139  evlslem4OLD  18152  evlslem4  18153  evlslem2  18159  evlslem6  18160  evlslem6OLD  18161  evlslem3  18162  evlslem1  18163  evlsval2  18168  psropprmul  18258  coe1mul2  18289  coe1tmmul2  18296  coe1tmmul  18297  ply1coe  18316  ply1coeOLD  18317  gsumsmonply1  18324  gsummoncoe1  18325  gsumfsum  18463  expmhm  18464  expghm  18507  expghmOLD  18508  mulgghm2  18509  mulgghm2OLD  18512  evpmodpmf1o  18610  isphld  18667  pjff  18721  frlmgsumOLD  18779  frlmgsum  18780  frlmsplit2  18781  frlmphl  18790  uvcff  18800  uvcresum  18802  frlmup1  18810  mamulid  18921  mamurid  18922  scmatf  19009  mdetf  19075  mdetunilem9  19100  mdetuni0  19101  mdetmul  19103  maduf  19121  smadiadetlem3lem1  19146  cpm2mf  19231  m2cpmfo  19235  pmatcollpw1  19255  pmatcollpw3lem  19262  pmatcollpw3fi1lem1  19265  pmatcollpw3fi1lem2  19266  pm2mpcl  19276  mply1topmatcl  19284  mp2pm2mplem2  19286  mp2pm2mp  19290  pm2mpmhmlem2  19298  chfacfisf  19333  chfacfisfcpmat  19334  cpmidpmatlem2  19350  cayhamlem4  19367  pptbas  19487  tgrest  19638  resttopon  19640  rest0  19648  restfpw  19658  ordtbaslem  19667  ordtuni  19669  ordtrest  19681  cnpfval  19713  pnrmopn  19822  cncmp  19870  discmp  19876  1stcfb  19924  2ndcomap  19937  dis2ndc  19939  lly1stc  19975  comppfsc  20011  kgencmp  20024  ptpjpre1  20050  ptpjcn  20090  ptcldmpt  20093  ptclsg  20094  dfac14  20097  xkoccn  20098  txcnp  20099  ptcnp  20101  txcnmpt  20103  uptx  20104  ptcn  20106  ptrescn  20118  txlm  20127  xkoptsub  20133  xkoco1cn  20136  xkoco2cn  20137  cnmpt11  20142  xkoinjcn  20166  kqffn  20204  pt1hmeo  20285  fbasrn  20363  trfilss  20368  trfg  20370  rnelfmlem  20431  txflf  20485  flfcnp2  20486  fclscmpi  20508  alexsublem  20522  ptcmplem3  20532  symgtgp  20578  subgntr  20583  opnsubg  20584  clsnsg  20586  tgpconcomp  20589  tsmsfbas  20604  eltsms  20609  haustsms  20612  tsmscls  20614  tsms0  20621  tsmsmhm  20626  tgptsmscls  20630  tsmssplit  20632  tsmsxplem1  20633  tsmsxplem2  20634  ustuqtop0  20721  prdsdsf  20848  prdsxmetlem  20849  imasdsf1olem  20854  prdsbl  20972  stdbdxmet  20996  met1stc  21002  nmf2  21091  nmof  21204  xrge0gsumle  21316  xrge0tsms  21317  metdsf  21330  metdsge  21331  mulc1cncf  21387  cncfmpt2ss  21397  cnmptre  21405  evth  21437  evth2  21438  lebnumlem1  21439  cphnmf  21620  tchcph  21658  cmetcaulem  21705  rrxmval  21810  minveclem1  21817  minveclem3b  21821  ovollb2lem  21877  ovolctb  21879  ovolunlem1a  21885  ovolunlem1  21886  ovoliunlem1  21891  ovoliunlem2  21892  ovoliun  21894  ovolshftlem1  21898  ovolscalem1  21902  ovolicc1  21905  iunmbl  21941  ioombl1lem1  21946  uniioombllem2  21970  uniioombllem3  21972  volsup2  21992  volcn  21993  vitalilem4  21998  vitalilem5  21999  mbfconst  22020  ismbfcn2  22024  mbfeqalem  22027  mbfss  22031  mbfmulc2re  22033  mbfmax  22034  mbfneg  22035  mbfpos  22036  mbfposr  22037  mbfposb  22038  mbfadd  22046  mbfmulc2  22048  mbfsup  22049  mbfinf  22050  mbflimsup  22051  mbflimlem  22052  mbflim  22053  i1f1lem  22074  i1f1  22075  i1fres  22090  itg1climres  22099  mbfi1fseqlem3  22102  mbfi1fseqlem4  22103  mbfi1flimlem  22107  mbfi1flim  22108  mbfmullem2  22109  mbfmul  22111  itg2const2  22126  itg2seq  22127  itg2splitlem  22133  itg2split  22134  itg2monolem1  22135  itg2monolem2  22136  itg2monolem3  22137  itg2mono  22138  itg2i1fseq  22140  itg2i1fseq2  22141  itg2gt0  22145  itg2cnlem1  22146  itg2cnlem2  22147  itg2cn  22148  iblss  22189  itgitg1  22193  itgle  22194  itgeqa  22198  itgss3  22199  ibladdlem  22204  itgaddlem1  22207  iblabslem  22212  iblabs  22213  iblabsr  22214  iblmulc2  22215  itgmulc2lem1  22216  bddmulibl  22223  itggt0  22226  itgcn  22227  ellimc2  22259  limcmpt  22265  limcres  22268  limccnp  22273  limccnp2  22274  limcco  22275  perfdvf  22285  dvreslem  22291  dvcnp2  22301  dvaddbr  22319  dvmulbr  22320  dvcjbr  22330  dvexp  22334  dvrec  22336  dvmptres3  22337  dvmptadd  22341  dvmptmul  22342  dvmptres2  22343  dvmptcmul  22345  dvmptcj  22349  dvmptntr  22352  dvmptco  22353  dvcnvlem  22355  dvef  22359  dvferm1  22364  dvferm2  22366  rolle  22369  dvlipcn  22373  dvle  22386  dvivthlem1  22387  dvivth  22389  lhop1lem  22392  lhop1  22393  lhop2  22394  lhop  22395  dvfsumle  22400  dvfsumge  22401  dvmptrecl  22403  dvfsumrlimf  22404  dvfsumlem2  22406  dvfsumlem3  22407  ftc1lem2  22415  ftc1lem6  22420  itgsubstlem  22427  tdeglem1  22434  tdeglem4  22436  coe1mul3  22478  elply2  22571  plyf  22573  elplyd  22577  plypf1  22587  coeeq2  22617  coemullem  22625  coe1termlem  22633  dvply2g  22659  elqaalem2  22694  taylfvallem  22731  taylf  22734  tayl0  22735  taylpfval  22738  taylpf  22739  taylthlem1  22746  taylthlem2  22747  ulmshftlem  22762  ulmshft  22763  ulmcau  22768  ulmss  22770  ulmdvlem1  22773  ulmdvlem3  22775  mtest  22777  mtestbdd  22778  itgulm2  22782  psergf  22785  radcnvlem1  22786  dvradcnv  22794  pserulm  22795  psercn2  22796  pserdvlem2  22801  abelthlem4  22807  abelthlem9  22813  pige3  22888  efif1olem4  22910  logtayl  23019  logccv  23022  loglesqrt  23110  leibpi  23251  rlimcnp  23273  rlimcnp2  23274  xrlimcnp  23276  efrlim  23277  dfef2  23278  o1cxp  23282  cxp2lim  23284  amgmlem  23297  basellem2  23333  basellem4  23335  basellem7  23338  basellem9  23340  sqff1o  23434  fsumvma  23466  dchrelbasd  23492  lgsfcl2  23555  lgsqrlem2  23595  lgseisenlem1  23602  lgseisenlem3  23604  lgseisenlem4  23605  chpo1ub  23643  dchrmusum2  23657  dchrvmasumiflem1  23664  dchrisum0ff  23670  dchrisum0lem1b  23678  dchrisum0lem2a  23680  logsqvma2  23706  pnt2  23776  pnt  23777  abvcxp  23778  padicabv  23793  lmif  24129  axlowdimlem15  24237  nbgraf1olem2  24420  wlkiswwlk2lem5  24673  wlknwwlknfun  24688  wlkiswwlkfun  24695  wwlkextfun  24707  clwlkisclwwlklem2a  24763  clwwlkf  24772  clwlkfclwwlk  24822  vdgrf  24876  vdgrfif  24877  frgrancvvdeqlem5  25012  numclwlk1lem2f  25070  numclwlk2lem2f  25081  efghgrpOLD  25353  ipblnfi  25749  ubthlem1  25764  minvecolem1  25768  htthlem  25812  hlimadd  26088  chscllem1  26533  hoaddcl  26655  homulcl  26656  brafn  26844  kbop  26850  cnlnadjlem2  26965  strlem3a  27149  hstrlem3a  27157  off2  27459  xppreima2  27466  fmpt3d  27474  fpwrelmap  27534  regsumfsum  27750  gsumvsca1  27751  gsumvsca2  27752  xrge0tsmsd  27753  ordtrestNEW  27881  xrge0mulc1cn  27901  esumf1o  28039  esumadd  28042  esumcst  28049  esumpfinval  28059  esumpcvgval  28062  esumcvg  28070  measinb  28170  measdivcst  28174  mbfmco2  28214  sitgclg  28262  eulerpartlems  28277  dstfrvclim1  28394  gsumncl  28470  gsumnunsn  28471  lgamgulmlem2  28550  lgamgulmlem6  28554  lgamcvg2  28575  gamcvg  28576  regamcl  28581  relgamcl  28582  erdszelem9  28621  indispcon  28657  cvxpcon  28665  cvmsss2  28697  cvmliftlem6  28713  cvmliftlem8  28715  cvmlift3lem3  28744  mrsubcv  28848  mrsubff  28850  mrsubrn  28851  mrsubccat  28856  elmrsubrn  28858  msubrn  28867  msubff  28868  mvhf  28896  divcnvlin  29096  iprodefisum  29100  faclimlem2  29145  faclim  29147  faclim2  29149  finixpnum  30014  ptrest  30024  mblfinlem2  30028  volsupnfl  30035  mbfposadd  30038  itg2addnclem2  30043  itg2gt0cn  30046  ibladdnclem  30047  itgaddnclem1  30049  itgaddnc  30051  iblabsnclem  30054  iblabsnc  30055  iblmulc2nc  30056  itgmulc2nclem1  30057  itgmulc2nclem2  30058  itgmulc2nc  30059  itgabsnc  30060  bddiblnc  30061  itggt0cn  30063  ftc1cnnc  30065  ftc1anclem1  30066  ftc1anclem2  30067  ftc1anclem3  30068  ftc1anclem4  30069  ftc1anclem5  30070  ftc1anclem6  30071  ftc1anclem7  30072  ftc1anclem8  30073  ftc1anc  30074  areacirclem4  30086  upixp  30196  totbndbnd  30261  prdsbnd  30265  cntotbnd  30268  rrnequiv  30307  cmpfiiin  30605  mzpclall  30635  mzpindd  30654  fphpdo  30727  dnnumch3  30969  kelac1  30985  dfac21  30988  itgpowd  31158  expgrowth  31216  rnmptc  31403  mptelpm  31407  expcnfg  31540  clim1fr1  31561  mullimc  31576  ellimcabssub0  31577  mullimcf  31583  constlimc  31584  idlimc  31586  sumnnodd  31590  neglimc  31607  addlimc  31608  0ellimcdiv  31609  cncfmptssg  31626  cncfshift  31630  cncfcompt  31639  icccncfext  31644  cncfiooiccre  31652  cxpcncf2  31657  dvsinax  31662  fperdvper  31669  dvmptresicc  31670  dvcosax  31677  ioodvbdlimc1lem1  31682  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  dvnmptdivc  31689  dvnxpaek  31693  dvnprodlem1  31697  dvnprodlem2  31698  dvnprodlem3  31699  itgsinexplem1  31706  iblsplit  31719  itgcoscmulx  31722  itgiccshift  31733  itgperiod  31734  itgsbtaddcnst  31735  dirkerf  31833  dirkeritg  31838  dirkercncflem2  31840  fourierdlem4  31847  fourierdlem5  31848  fourierdlem9  31852  fourierdlem14  31857  fourierdlem16  31859  fourierdlem17  31860  fourierdlem18  31861  fourierdlem21  31864  fourierdlem22  31865  fourierdlem37  31880  fourierdlem50  31893  fourierdlem51  31894  fourierdlem53  31896  fourierdlem55  31898  fourierdlem57  31900  fourierdlem58  31901  fourierdlem59  31902  fourierdlem60  31903  fourierdlem61  31904  fourierdlem67  31910  fourierdlem68  31911  fourierdlem72  31915  fourierdlem73  31916  fourierdlem74  31917  fourierdlem75  31918  fourierdlem76  31919  fourierdlem78  31921  fourierdlem80  31923  fourierdlem81  31924  fourierdlem83  31926  fourierdlem84  31927  fourierdlem88  31931  fourierdlem92  31935  fourierdlem93  31936  fourierdlem97  31940  fourierdlem101  31944  fourierdlem103  31946  fourierdlem104  31947  fourierdlem111  31954  sqwvfoura  31965  elaa2lem  31970  etransclem1  31972  etransclem8  31979  etransclem20  31991  etransclem33  32004  etransclem35  32006  etransclem39  32010  funcestrcsetclem3  32614  funcsetcestrclem3  32628  funcringcsetcOLD2lem3  32718  funcringcsetclem3OLD  32741  gsumlsscl  32846  ply1mulgsum  32860  lincfsuppcl  32884  linccl  32885  lincvalsc0  32892  lcoc0  32893  linc0scn0  32894  linc1  32896  lincsum  32900  lincscm  32901  lincscmcl  32903  lcoss  32907  lincext1  32925  el0ldep  32937  lincresunit1  32948  lincresunit3  32952  lmod1zr  32964  lsatlss  34596  lflnegcl  34675  lshpkrcl  34716  tendoplcl  36382  tendo0cl  36391  tendoicl  36397
  Copyright terms: Public domain W3C validator