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

Theorem fmptd 5855
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 2789 . 2  |-  ( ph  ->  A. x  e.  A  B  e.  C )
3 fmptd.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43fmpt 5852 . 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 1362    e. wcel 1755   A.wral 2705    e. cmpt 4338   -->wf 5402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-fv 5414
This theorem is referenced by:  fmptco  5863  fliftrel  5988  off  6323  caofinvl  6336  curry1f  6655  curry2f  6657  fnwelem  6676  fdiagfn  7244  resixpfo  7289  pw2f1olem  7403  mapxpen  7465  xpmapenlem  7466  unxpdomlem3  7507  fsuppmptdm  7619  fsuppmptif  7637  wdom2d  7783  cantnfp1lem1  7874  cantnfp1lem2  7875  cantnfp1lem3  7876  cantnflem1d  7884  cantnflem1  7885  cantnf  7889  cantnfp1lem1OLD  7900  cantnfp1lem2OLD  7901  cantnfp1lem3OLD  7902  cantnflem1dOLD  7907  cantnflem1OLD  7908  cantnfOLD  7911  fseqenlem1  8182  fseqenlem2  8183  dfac8clem  8190  ac5num  8194  acni2  8204  infpwfien  8220  coftr  8430  fin23lem39  8507  isf34lem2  8530  fin1a2lem12  8568  axcc2lem  8593  axdc2lem  8605  axdc3lem4  8610  pwcfsdom  8735  canthp1lem2  8808  wuncval2  8902  gruf  8966  rpnnen1lem1  10967  monoord2  11821  seqf1o  11831  ccatcl  12258  swrdcl  12299  revcl  12385  revlen  12386  ello1mpt  12983  lo1o12  12995  lo1eq  13030  rlimeq  13031  climmpt2  13035  rlimcld2  13040  climrecl  13045  climge0  13046  o1compt  13049  rlimcn1b  13051  rlimcn2  13052  rlimdiv  13107  rlimsqzlem  13110  isercoll2  13130  caurcvg2  13139  caucvg  13140  sumrblem  13172  summolem2a  13176  fsumf1o  13184  sumss  13185  fsumss  13186  fsumcl2lem  13192  fsumadd  13199  isumclim3  13210  isummulc2  13213  fsummulc2  13234  fsumrelem  13253  climfsum  13266  isumshft  13285  divcnv  13299  supcvg  13301  rpnnen2lem2  13481  crt  13836  eulerthlem1  13839  iserodd  13885  prmreclem2  13961  prmreclem6  13965  1arithlem3  13969  4sqlem11  13999  vdwapf  14016  vdwlem2  14026  vdwlem4  14028  vdwlem6  14030  vdwlem10  14034  ramub1lem2  14071  ramcl  14073  prdsplusg  14379  prdsmulr  14380  prdsvsca  14381  mrcflem  14527  mreacs  14579  acsfn  14580  homaf  14881  prfcl  14996  curf1cl  15021  hofcllem  15051  hofcl  15052  yonedalem3a  15067  yonedalem4c  15070  yonedainv  15074  prdspjmhm  15477  pwsco1mhm  15480  pwsco2mhm  15481  gsumz  15491  gsumwspan  15504  vrmdfval  15514  vrmdf  15516  frmdup1  15522  grpinvf  15562  cycsubgcl  15687  cycsubgss  15688  conjghm  15757  conjnmz  15760  divsghm  15763  galactghm  15888  symgextf  15902  symgfixf  15922  pmtrf  15941  psgnunilem5  15980  odf1  16043  dfod2  16045  odf1o2  16052  pgpssslw  16093  sylow2blem1  16099  pj1f  16174  frgpmhm  16242  vrgpf  16245  mulgmhm  16295  mulgghm  16296  iscyggen2  16338  cyggenod  16341  iscyg3  16343  gsummptfsadd  16394  gsummptfsaddOLD  16395  gsumzsplit  16398  gsumzsplitOLD  16399  gsumsplit2  16402  gsumsplit2OLD  16403  gsummptfidmsplitres  16405  gsumconst  16406  gsummhm2  16411  gsummhm2OLD  16412  gsummptfidminv  16421  gsummptif1n0  16431  gsum2dlem1  16435  gsum2dlem2  16436  gsum2d  16437  gsum2dOLD  16438  prdsgsum  16445  prdsgsumOLD  16446  dprdfeq0  16486  dprdfeq0OLD  16493  dprdlub  16497  dprdz  16501  dprd2dlem1  16514  dprd2da  16515  ablfac1b  16545  ablfac2  16564  rnglghm  16628  rngrghm  16629  gsumdixpOLD  16635  gsumdixp  16636  abvtrivd  16849  issrngd  16870  lmodvsghm  16930  lspf  16977  pwssplit0  17061  asclf  17330  snifpsrbag  17367  psrass1lem  17381  psrbasOLD  17383  psrmulcllem  17392  psr1cl  17407  psrlidm  17408  psrlidmOLD  17409  psrridm  17410  psrridmOLD  17411  psrdi  17413  psrdir  17414  psrcom  17415  resspsrmul  17423  subrgpsr  17425  mvridlemOLD  17426  mvrf  17431  mplmon  17476  mplmonmul  17477  mplcoe1  17478  mplcoe3OLD  17480  mplcoe2  17481  mplcoe2OLD  17482  mplbas2  17483  mplbas2OLD  17484  psrbagsn  17509  evlslem4OLD  17518  evlslem4  17519  evlslem2  17525  psropprmul  17591  coe1mul2  17621  coe1tmmul2  17627  coe1tmmul  17628  ply1coe  17643  gsumfsum  17723  expmhm  17724  expghm  17765  expghmOLD  17766  mulgghm2  17767  mulgghm2OLD  17770  evpmodpmf1o  17868  isphld  17925  pjff  17979  frlmgsumOLD  18037  frlmgsum  18038  frlmsplit2  18039  frlmphl  18048  uvcff  18058  uvcresum  18060  frlmup1  18068  mamulid  18146  mamurid  18147  mdetf  18248  mdetunilem9  18268  mdetuni0  18269  mdetmul  18271  maduf  18289  pptbas  18454  tgrest  18605  resttopon  18607  rest0  18615  restfpw  18625  ordtbaslem  18634  ordtuni  18636  ordtrest  18648  cnpfval  18680  pnrmopn  18789  cncmp  18837  discmp  18843  1stcfb  18891  2ndcomap  18904  dis2ndc  18906  lly1stc  18942  kgencmp  18960  ptpjpre1  18986  ptpjcn  19026  ptcldmpt  19029  ptclsg  19030  dfac14  19033  xkoccn  19034  txcnp  19035  ptcnp  19037  txcnmpt  19039  uptx  19040  ptcn  19042  ptrescn  19054  txlm  19063  xkoptsub  19069  xkoco1cn  19072  xkoco2cn  19073  cnmpt11  19078  xkoinjcn  19102  kqffn  19140  pt1hmeo  19221  fbasrn  19299  trfilss  19304  trfg  19306  rnelfmlem  19367  txflf  19421  flfcnp2  19422  fclscmpi  19444  alexsublem  19458  ptcmplem3  19468  symgtgp  19514  subgntr  19519  opnsubg  19520  clsnsg  19522  tgpconcomp  19525  tsmsfbas  19540  eltsms  19545  haustsms  19548  tsmscls  19550  tsms0  19557  tsmsmhm  19562  tgptsmscls  19566  tsmssplit  19568  tsmsxplem1  19569  tsmsxplem2  19570  ustuqtop0  19657  prdsdsf  19784  prdsxmetlem  19785  imasdsf1olem  19790  prdsbl  19908  stdbdxmet  19932  met1stc  19938  nmf2  20027  nmof  20140  xrge0gsumle  20252  xrge0tsms  20253  metdsf  20266  metdsge  20267  mulc1cncf  20323  cncfmpt2ss  20333  cnmptre  20341  evth  20373  evth2  20374  lebnumlem1  20375  cphnmf  20556  tchcph  20594  cmetcaulem  20641  rrxmval  20746  minveclem1  20753  minveclem3b  20757  ovollb2lem  20813  ovolctb  20815  ovolunlem1a  20821  ovolunlem1  20822  ovoliunlem1  20827  ovoliunlem2  20828  ovoliun  20830  ovolshftlem1  20834  ovolscalem1  20838  ovolicc1  20841  iunmbl  20876  ioombl1lem1  20881  uniioombllem2  20905  uniioombllem3  20907  volsup2  20927  volcn  20928  vitalilem4  20933  vitalilem5  20934  mbfconst  20955  ismbfcn2  20959  mbfeqalem  20962  mbfss  20966  mbfmulc2re  20968  mbfmax  20969  mbfneg  20970  mbfpos  20971  mbfposr  20972  mbfposb  20973  mbfadd  20981  mbfmulc2  20983  mbfsup  20984  mbfinf  20985  mbflimsup  20986  mbflimlem  20987  mbflim  20988  i1f1lem  21009  i1f1  21010  i1fres  21025  itg1climres  21034  mbfi1fseqlem3  21037  mbfi1fseqlem4  21038  mbfi1flimlem  21042  mbfi1flim  21043  mbfmullem2  21044  mbfmul  21046  itg2const2  21061  itg2seq  21062  itg2splitlem  21068  itg2split  21069  itg2monolem1  21070  itg2monolem2  21071  itg2monolem3  21072  itg2mono  21073  itg2i1fseq  21075  itg2i1fseq2  21076  itg2gt0  21080  itg2cnlem1  21081  itg2cnlem2  21082  itg2cn  21083  isibl2  21086  iblss  21124  itgitg1  21128  itgle  21129  itgeqa  21133  itgss3  21134  ibladdlem  21139  itgaddlem1  21142  iblabslem  21147  iblabs  21148  iblabsr  21149  iblmulc2  21150  itgmulc2lem1  21151  bddmulibl  21158  itggt0  21161  itgcn  21162  ellimc2  21194  limcmpt  21200  limcres  21203  limccnp  21208  limccnp2  21209  limcco  21210  perfdvf  21220  dvreslem  21226  dvcnp2  21236  dvaddbr  21254  dvmulbr  21255  dvcjbr  21265  dvexp  21269  dvrec  21271  dvmptres3  21272  dvmptadd  21276  dvmptmul  21277  dvmptres2  21278  dvmptcmul  21280  dvmptcj  21284  dvmptntr  21287  dvmptco  21288  dvcnvlem  21290  dvef  21294  dvferm1  21299  dvferm2  21301  rolle  21304  dvlipcn  21308  dvle  21321  dvivthlem1  21322  dvivth  21324  lhop1lem  21327  lhop1  21328  lhop2  21329  lhop  21330  dvfsumle  21335  dvfsumge  21336  dvmptrecl  21338  dvfsumrlimf  21339  dvfsumlem2  21341  dvfsumlem3  21342  ftc1lem2  21350  ftc1lem6  21355  itgsubstlem  21362  evlslem6  21364  evlslem6OLD  21365  evlslem3  21366  evlslem1  21367  evlsval2  21372  tdeglem1  21412  tdeglem4  21414  coe1mul3  21456  elply2  21549  plyf  21551  elplyd  21555  plypf1  21565  coeeq2  21595  coemullem  21602  coe1termlem  21610  dvply2g  21636  elqaalem2  21671  taylfvallem  21708  taylf  21711  tayl0  21712  taylpfval  21715  taylpf  21716  taylthlem1  21723  taylthlem2  21724  ulmshftlem  21739  ulmshft  21740  ulmcau  21745  ulmss  21747  ulmdvlem1  21750  ulmdvlem3  21752  mtest  21754  mtestbdd  21755  iblulm  21757  itgulm2  21759  psergf  21762  radcnvlem1  21763  dvradcnv  21771  pserulm  21772  psercn2  21773  pserdvlem2  21778  abelthlem4  21784  abelthlem9  21790  pige3  21864  efif1olem4  21886  logtayl  21990  logccv  21993  loglesqr  22081  leibpi  22222  rlimcnp  22244  rlimcnp2  22245  xrlimcnp  22247  efrlim  22248  dfef2  22249  o1cxp  22253  cxp2lim  22255  amgmlem  22268  basellem2  22304  basellem4  22306  basellem7  22309  basellem9  22311  sqff1o  22405  fsumvma  22437  dchrelbasd  22463  lgsfcl2  22526  lgsqrlem2  22566  lgseisenlem1  22573  lgseisenlem3  22575  lgseisenlem4  22576  chpo1ub  22614  dchrisumlema  22622  dchrmusum2  22628  dchrvmasumiflem1  22635  dchrisum0ff  22641  dchrisum0lem1b  22649  dchrisum0lem2a  22651  logsqvma2  22677  pnt2  22747  pnt  22748  abvcxp  22749  padicabv  22764  axlowdimlem15  23025  nbgraf1olem2  23174  vdgrf  23391  vdgrfif  23392  efghgrp  23683  ipblnfi  24079  ubthlem1  24094  minvecolem1  24098  htthlem  24142  hlimadd  24418  chscllem1  24863  hoaddcl  24985  homulcl  24986  brafn  25174  kbop  25180  cnlnadjlem2  25295  strlem3a  25479  hstrlem3a  25487  off2  25783  xppreima2  25789  fmpt3d  25797  fpwrelmap  25858  gsummptf1o  26099  gsummptun  26100  gsummptmhm  26102  regsumfsum  26103  gsumvsca1  26104  gsumvsca2  26105  xrge0tsmsd  26106  ordtrestNEW  26205  xrge0mulc1cn  26225  esumf1o  26358  esumadd  26361  esumcst  26368  esumpfinval  26378  esumpcvgval  26381  esumcvg  26389  measinb  26489  measdivcst  26493  mbfmco2  26534  sitgclg  26576  eulerpartlems  26591  dstfrvclim1  26708  gsumncl  26784  gsumnunsn  26785  signstf  26815  lgamgulmlem2  26864  lgamgulmlem6  26868  lgamcvg2  26889  gamcvg  26890  regamcl  26895  relgamcl  26896  erdszelem9  26935  indispcon  26971  cvxpcon  26979  cvmsss2  27011  cvmliftlem6  27027  cvmliftlem8  27029  cvmlift3lem3  27058  divcnvlin  27246  prodfdiv  27258  prodrblem  27289  prodmolem2a  27294  fprodf1o  27306  prodss  27307  fprodss  27308  fprodser  27309  fprodcl2lem  27310  fprodmul  27318  fproddiv  27319  fprodefsum  27332  fprodn0  27337  iprodclim3  27347  iprodefisum  27352  faclimlem2  27397  faclim  27399  faclim2  27401  finixpnum  28258  ptrest  28269  mblfinlem2  28273  volsupnfl  28280  mbfposadd  28283  itg2addnclem2  28288  itg2gt0cn  28291  ibladdnclem  28292  itgaddnclem1  28294  itgaddnc  28296  iblabsnclem  28299  iblabsnc  28300  iblmulc2nc  28301  itgmulc2nclem1  28302  itgmulc2nclem2  28303  itgmulc2nc  28304  itgabsnc  28305  bddiblnc  28306  itggt0cn  28308  ftc1cnnc  28310  ftc1anclem1  28311  ftc1anclem2  28312  ftc1anclem3  28313  ftc1anclem4  28314  ftc1anclem5  28315  ftc1anclem6  28316  ftc1anclem7  28317  ftc1anclem8  28318  ftc1anc  28319  areacirclem4  28331  comppfsc  28423  upixp  28467  totbndbnd  28532  prdsbnd  28536  cntotbnd  28539  rrnequiv  28578  cmpfiiin  28878  mzpclall  28908  mzpindd  28927  fphpdo  29001  dnnumch3  29245  kelac1  29261  dfac21  29264  itgpowd  29435  expgrowth  29454  expcnfg  29619  clim1fr1  29620  itgsinexplem1  29640  wlkiswwlk2lem5  30175  wlknwwlknfun  30188  wlkiswwlkfun  30195  wwlkextfun  30207  clwlkisclwwlklem2a  30293  clwwlkf  30302  clwlkfclwwlk  30363  frgrancvvdeqlem5  30473  numclwlk1lem2f  30531  numclwlk2lem2f  30542  gsumlsscl  30625  lincfsuppcl  30656  linccl  30657  lincvalsc0  30664  lcoc0  30665  linc0scn0  30666  linc1  30668  lincsum  30672  lincscm  30673  lincscmcl  30675  lcoss  30679  lincext1  30697  el0ldep  30709  lincresunit1  30720  lincresunit3  30724  lmod1zr  30744  lsatlss  32214  lflnegcl  32293  lshpkrcl  32334  tendoplcl  33998  tendo0cl  34007  tendoicl  34013
  Copyright terms: Public domain W3C validator