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

Theorem fmptd 5885
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 2781 . 2  |-  ( ph  ->  A. x  e.  A  B  e.  C )
3 fmptd.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43fmpt 5882 . 2  |-  ( A. x  e.  A  B  e.  C  <->  F : A --> C )
52, 4sylib 189 1  |-  ( ph  ->  F : A --> C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    e. wcel 1725   A.wral 2697    e. cmpt 4258   -->wf 5442
This theorem is referenced by:  fmptco  5893  fliftrel  6022  off  6312  caofinvl  6323  curry1f  6432  curry2f  6434  fnwelem  6453  fdiagfn  7049  resixpfo  7092  pw2f1olem  7204  mapxpen  7265  xpmapenlem  7266  unxpdomlem3  7307  wdom2d  7540  cantnfp1lem1  7626  cantnfp1lem2  7627  cantnfp1lem3  7628  cantnflem1d  7636  cantnflem1  7637  cantnf  7641  fseqenlem1  7897  fseqenlem2  7898  dfac8clem  7905  ac5num  7909  acni2  7919  infpwfien  7935  coftr  8145  fin23lem39  8222  isf34lem2  8245  fin1a2lem12  8283  axcc2lem  8308  axdc2lem  8320  axdc3lem4  8325  pwcfsdom  8450  canthp1lem2  8520  wuncval2  8614  gruf  8678  rpnnen1lem1  10592  monoord2  11346  seqf1o  11356  ccatcl  11735  swrdcl  11758  revcl  11785  revlen  11786  ello1mpt  12307  lo1o12  12319  lo1eq  12354  rlimeq  12355  climmpt2  12359  rlimcld2  12364  climrecl  12369  climge0  12370  o1compt  12373  rlimcn1b  12375  rlimcn2  12376  rlimdiv  12431  rlimsqzlem  12434  isercoll2  12454  caurcvg2  12463  caucvg  12464  sumrblem  12497  summolem2a  12501  fsumf1o  12509  sumss  12510  fsumss  12511  fsumcl2lem  12517  fsumadd  12524  isumclim3  12535  isummulc2  12538  fsummulc2  12559  fsumrelem  12578  climfsum  12591  isumshft  12611  divcnv  12625  supcvg  12627  rpnnen2lem2  12807  crt  13159  eulerthlem1  13162  iserodd  13201  prmreclem2  13277  prmreclem6  13281  1arithlem3  13285  4sqlem11  13315  vdwapf  13332  vdwlem2  13342  vdwlem4  13344  vdwlem6  13346  vdwlem10  13350  ramub1lem2  13387  ramcl  13389  prdsplusg  13673  prdsmulr  13674  prdsvsca  13675  mrcflem  13823  mreacs  13875  acsfn  13876  homaf  14177  prfcl  14292  curf1cl  14317  hofcllem  14347  hofcl  14348  yonedalem3a  14363  yonedalem4c  14366  yonedainv  14370  prdspjmhm  14758  pwsco1mhm  14761  pwsco2mhm  14762  gsumz  14773  gsumwspan  14783  vrmdfval  14793  vrmdf  14795  frmdup1  14801  grpinvf  14841  cycsubgcl  14958  cycsubgss  14959  conjghm  15028  conjnmz  15031  divsghm  15034  galactghm  15098  odf1  15190  dfod2  15192  odf1o2  15199  pgpssslw  15240  sylow2blem1  15246  pj1f  15321  frgpmhm  15389  vrgpf  15392  mulgmhm  15442  mulgghm  15443  iscyggen2  15483  cyggenod  15486  iscyg3  15488  gsumzsplit  15521  gsumsplit2  15523  gsumconst  15524  gsummhm2  15527  gsum2d  15538  prdsgsum  15544  dprdfeq0  15572  dprdlub  15576  dprdz  15580  dprd2dlem1  15591  dprd2da  15592  ablfac1b  15620  ablfac2  15639  rnglghm  15703  rngrghm  15704  gsumdixp  15707  abvtrivd  15920  issrngd  15941  lmodvsghm  15997  lspf  16042  asclf  16388  psrass1lem  16434  psrbas  16435  psrmulcllem  16443  psr1cl  16458  psrlidm  16459  psrridm  16460  psrass1  16461  psrdi  16462  psrdir  16463  psrcom  16464  resspsrmul  16472  subrgpsr  16474  mvridlem  16475  mvrf  16480  mplmon  16518  mplmonmul  16519  mplcoe1  16520  mplcoe3  16521  mplcoe2  16522  mplbas2  16523  psrbagsn  16547  evlslem4  16556  evlslem2  16560  psropprmul  16624  coe1mul2  16654  coe1tmmul2  16660  coe1tmmul  16661  ply1coe  16676  gsumfsum  16758  expmhm  16768  expghm  16769  mulgghm2  16778  isphld  16877  pjff  16931  pptbas  17064  tgrest  17215  resttopon  17217  rest0  17225  restfpw  17235  ordtbaslem  17244  ordtuni  17246  ordtrest  17258  cnpfval  17290  pnrmopn  17399  cncmp  17447  discmp  17453  1stcfb  17500  2ndcomap  17513  dis2ndc  17515  lly1stc  17551  kgencmp  17569  ptpjpre1  17595  ptpjcn  17635  ptcldmpt  17638  ptclsg  17639  dfac14  17642  xkoccn  17643  txcnp  17644  ptcnp  17646  txcnmpt  17648  uptx  17649  ptcn  17651  ptrescn  17663  txlm  17672  xkoptsub  17678  xkoco1cn  17681  xkoco2cn  17682  cnmpt11  17687  xkoinjcn  17711  kqffn  17749  pt1hmeo  17830  fbasrn  17908  trfilss  17913  trfg  17915  rnelfmlem  17976  txflf  18030  flfcnp2  18031  fclscmpi  18053  alexsublem  18067  ptcmplem3  18077  symgtgp  18123  subgntr  18128  opnsubg  18129  clsnsg  18131  tgpconcomp  18134  tsmsfbas  18149  eltsms  18154  haustsms  18157  tsmscls  18159  tsms0  18163  tsmsmhm  18167  tgptsmscls  18171  tsmssplit  18173  tsmsxplem1  18174  tsmsxplem2  18175  ustuqtop0  18262  prdsdsf  18389  prdsxmetlem  18390  imasdsf1olem  18395  prdsbl  18513  stdbdxmet  18537  met1stc  18543  nmf2  18632  nmof  18745  xrge0gsumle  18856  xrge0tsms  18857  metdsf  18870  metdsge  18871  mulc1cncf  18927  cncfmpt2ss  18937  cnmptre  18944  evth  18976  evth2  18977  lebnumlem1  18978  cphnmf  19150  tchcph  19186  cmetcaulem  19233  minveclem1  19317  minveclem3b  19321  ovollb2lem  19376  ovolctb  19378  ovolunlem1a  19384  ovolunlem1  19385  ovoliunlem1  19390  ovoliunlem2  19391  ovoliun  19393  ovolshftlem1  19397  ovolscalem1  19401  ovolicc1  19404  iunmbl  19439  ioombl1lem1  19444  uniioombllem2  19467  uniioombllem3  19469  volsup2  19489  volcn  19490  vitalilem4  19495  vitalilem5  19496  mbfconst  19519  ismbfcn2  19523  mbfeqalem  19526  mbfss  19530  mbfmulc2re  19532  mbfmax  19533  mbfneg  19534  mbfpos  19535  mbfposr  19536  mbfposb  19537  mbfadd  19545  mbfmulc2  19547  mbfsup  19548  mbfinf  19549  mbflimsup  19550  mbflimlem  19551  mbflim  19552  i1f1lem  19573  i1f1  19574  i1fres  19589  itg1climres  19598  mbfi1fseqlem3  19601  mbfi1fseqlem4  19602  mbfi1flimlem  19606  mbfi1flim  19607  mbfmullem2  19608  mbfmul  19610  itg2const2  19625  itg2seq  19626  itg2splitlem  19632  itg2split  19633  itg2monolem1  19634  itg2monolem2  19635  itg2monolem3  19636  itg2mono  19637  itg2i1fseq  19639  itg2i1fseq2  19640  itg2gt0  19644  itg2cnlem1  19645  itg2cnlem2  19646  itg2cn  19647  isibl2  19650  iblss  19688  itgitg1  19692  itgle  19693  itgeqa  19697  itgss3  19698  ibladdlem  19703  itgaddlem1  19706  iblabslem  19711  iblabs  19712  iblabsr  19713  iblmulc2  19714  itgmulc2lem1  19715  bddmulibl  19722  itggt0  19725  itgcn  19726  ellimc2  19756  limcmpt  19762  limcres  19765  limccnp  19770  limccnp2  19771  limcco  19772  perfdvf  19782  dvreslem  19788  dvcnp2  19798  dvaddbr  19816  dvmulbr  19817  dvcjbr  19827  dvexp  19831  dvrec  19833  dvmptres3  19834  dvmptadd  19838  dvmptmul  19839  dvmptres2  19840  dvmptcmul  19842  dvmptcj  19846  dvmptntr  19849  dvmptco  19850  dvcnvlem  19852  dvef  19856  dvferm1  19861  dvferm2  19863  rolle  19866  dvlipcn  19870  dvle  19883  dvivthlem1  19884  dvivth  19886  lhop1lem  19889  lhop1  19890  lhop2  19891  lhop  19892  dvfsumle  19897  dvfsumge  19898  dvmptrecl  19900  dvfsumrlimf  19901  dvfsumlem2  19903  dvfsumlem3  19904  ftc1lem2  19912  ftc1lem6  19917  itgsubstlem  19924  evlslem6  19926  evlslem3  19927  evlslem1  19928  evlsval2  19933  tdeglem1  19973  tdeglem4  19975  coe1mul3  20014  elply2  20107  plyf  20109  elplyd  20113  plypf1  20123  coeeq2  20153  coemullem  20160  coe1termlem  20168  dvply2g  20194  elqaalem2  20229  taylfvallem  20266  taylf  20269  tayl0  20270  taylpfval  20273  taylpf  20274  taylthlem1  20281  taylthlem2  20282  ulmshftlem  20297  ulmshft  20298  ulmcau  20303  ulmss  20305  ulmdvlem1  20308  ulmdvlem3  20310  mtest  20312  mtestbdd  20313  iblulm  20315  itgulm2  20317  psergf  20320  radcnvlem1  20321  dvradcnv  20329  pserulm  20330  psercn2  20331  pserdvlem2  20336  abelthlem4  20342  abelthlem9  20348  pige3  20417  efif1olem4  20439  logtayl  20543  logccv  20546  loglesqr  20634  leibpi  20774  rlimcnp  20796  rlimcnp2  20797  xrlimcnp  20799  efrlim  20800  dfef2  20801  o1cxp  20805  cxp2lim  20807  amgmlem  20820  basellem2  20856  basellem4  20858  basellem7  20861  basellem9  20863  sqff1o  20957  fsumvma  20989  dchrelbasd  21015  lgsfcl2  21078  lgsqrlem2  21118  lgseisenlem1  21125  lgseisenlem3  21127  lgseisenlem4  21128  chpo1ub  21166  dchrisumlema  21174  dchrmusum2  21180  dchrvmasumiflem1  21187  dchrisum0ff  21193  dchrisum0lem1b  21201  dchrisum0lem2a  21203  logsqvma2  21229  pnt2  21299  pnt  21300  abvcxp  21301  padicabv  21316  nbgraf1olem2  21444  vdgrf  21661  vdgrfif  21662  efghgrp  21953  ipblnfi  22349  ubthlem1  22364  minvecolem1  22368  htthlem  22412  hlimadd  22687  chscllem1  23131  hoaddcl  23253  homulcl  23254  brafn  23442  kbop  23448  cnlnadjlem2  23563  strlem3a  23747  hstrlem3a  23755  off2  24046  xppreima2  24052  fmpt3d  24062  xrge0tsmsd  24215  xrge0mulc1cn  24319  esumf1o  24437  esumadd  24440  esumcst  24447  esumpfinval  24457  esumpcvgval  24460  esumcvg  24468  measinb  24567  measdivcst  24571  mbfmco2  24607  sitgclg  24648  dstfrvclim1  24727  lgamgulmlem2  24806  lgamgulmlem6  24810  lgamcvg2  24831  gamcvg  24832  regamcl  24837  relgamcl  24838  erdszelem9  24877  indispcon  24913  cvxpcon  24921  cvmsss2  24953  cvmliftlem6  24969  cvmliftlem8  24971  cvmlift3lem3  25000  divcnvlin  25204  prodfdiv  25216  prodrblem  25247  prodmolem2a  25252  fprodf1o  25264  prodss  25265  fprodss  25266  fprodser  25267  fprodcl2lem  25268  fprodmul  25276  fproddiv  25277  fprodefsum  25290  fprodn0  25295  iprodclim3  25305  iprodefisum  25310  faclimlem2  25355  faclim  25357  faclim2  25359  axlowdimlem15  25887  mblfinlem  26234  volsupnfl  26241  mbfposadd  26244  itg2addnclem2  26247  itg2gt0cn  26250  ibladdnclem  26251  itgaddnclem1  26253  itgaddnc  26255  iblabsnclem  26258  iblabsnc  26259  iblmulc2nc  26260  itgmulc2nclem1  26261  itgmulc2nclem2  26262  itgmulc2nc  26263  itgabsnc  26264  bddiblnc  26265  itggt0cn  26267  ftc1cnnc  26269  ftc1anclem1  26270  ftc1anclem2  26271  ftc1anclem3  26272  ftc1anclem4  26273  ftc1anclem5  26274  ftc1anclem6  26275  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  areacirclem3  26283  areacirclem5  26286  comppfsc  26378  upixp  26422  totbndbnd  26489  prdsbnd  26493  cntotbnd  26496  rrnequiv  26535  cmpfiiin  26742  mzpclall  26775  mzpindd  26794  fphpdo  26869  dnnumch3  27113  kelac1  27129  dfac21  27132  pwssplit0  27155  frlmgsum  27200  uvcff  27208  uvcresum  27210  frlmsplit2  27211  frlmup1  27218  pmtrf  27365  psgnunilem5  27385  mamucl  27424  mamulid  27426  mamurid  27427  mamuass  27428  mamudi  27429  mamudir  27430  mamuvs1  27431  mamuvs2  27432  expgrowth  27520  expcnfg  27693  clim1fr1  27694  itgsinexplem1  27715  frgrancvvdeqlem5  28360  lsatlss  29731  lflnegcl  29810  lshpkrcl  29851  tendoplcl  31515  tendo0cl  31524  tendoicl  31530
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-fv 5454
  Copyright terms: Public domain W3C validator