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

Theorem fmptd 5895
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 5892 . 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 4268   -->wf 5452
This theorem is referenced by:  fmptco  5903  fliftrel  6032  off  6322  caofinvl  6333  curry1f  6442  curry2f  6444  fnwelem  6463  fdiagfn  7059  resixpfo  7102  pw2f1olem  7214  mapxpen  7275  xpmapenlem  7276  unxpdomlem3  7317  wdom2d  7550  cantnfp1lem1  7636  cantnfp1lem2  7637  cantnfp1lem3  7638  cantnflem1d  7646  cantnflem1  7647  cantnf  7651  fseqenlem1  7907  fseqenlem2  7908  dfac8clem  7915  ac5num  7919  acni2  7929  infpwfien  7945  coftr  8155  fin23lem39  8232  isf34lem2  8255  fin1a2lem12  8293  axcc2lem  8318  axdc2lem  8330  axdc3lem4  8335  pwcfsdom  8460  canthp1lem2  8530  wuncval2  8624  gruf  8688  rpnnen1lem1  10602  monoord2  11356  seqf1o  11366  ccatcl  11745  swrdcl  11768  revcl  11795  revlen  11796  ello1mpt  12317  lo1o12  12329  lo1eq  12364  rlimeq  12365  climmpt2  12369  rlimcld2  12374  climrecl  12379  climge0  12380  o1compt  12383  rlimcn1b  12385  rlimcn2  12386  rlimdiv  12441  rlimsqzlem  12444  isercoll2  12464  caurcvg2  12473  caucvg  12474  sumrblem  12507  summolem2a  12511  fsumf1o  12519  sumss  12520  fsumss  12521  fsumcl2lem  12527  fsumadd  12534  isumclim3  12545  isummulc2  12548  fsummulc2  12569  fsumrelem  12588  climfsum  12601  isumshft  12621  divcnv  12635  supcvg  12637  rpnnen2lem2  12817  crt  13169  eulerthlem1  13172  iserodd  13211  prmreclem2  13287  prmreclem6  13291  1arithlem3  13295  4sqlem11  13325  vdwapf  13342  vdwlem2  13352  vdwlem4  13354  vdwlem6  13356  vdwlem10  13360  ramub1lem2  13397  ramcl  13399  prdsplusg  13683  prdsmulr  13684  prdsvsca  13685  mrcflem  13833  mreacs  13885  acsfn  13886  homaf  14187  prfcl  14302  curf1cl  14327  hofcllem  14357  hofcl  14358  yonedalem3a  14373  yonedalem4c  14376  yonedainv  14380  prdspjmhm  14768  pwsco1mhm  14771  pwsco2mhm  14772  gsumz  14783  gsumwspan  14793  vrmdfval  14803  vrmdf  14805  frmdup1  14811  grpinvf  14851  cycsubgcl  14968  cycsubgss  14969  conjghm  15038  conjnmz  15041  divsghm  15044  galactghm  15108  odf1  15200  dfod2  15202  odf1o2  15209  pgpssslw  15250  sylow2blem1  15256  pj1f  15331  frgpmhm  15399  vrgpf  15402  mulgmhm  15452  mulgghm  15453  iscyggen2  15493  cyggenod  15496  iscyg3  15498  gsumzsplit  15531  gsumsplit2  15533  gsumconst  15534  gsummhm2  15537  gsum2d  15548  prdsgsum  15554  dprdfeq0  15582  dprdlub  15586  dprdz  15590  dprd2dlem1  15601  dprd2da  15602  ablfac1b  15630  ablfac2  15649  rnglghm  15713  rngrghm  15714  gsumdixp  15717  abvtrivd  15930  issrngd  15951  lmodvsghm  16007  lspf  16052  asclf  16398  psrass1lem  16444  psrbas  16445  psrmulcllem  16453  psr1cl  16468  psrlidm  16469  psrridm  16470  psrass1  16471  psrdi  16472  psrdir  16473  psrcom  16474  resspsrmul  16482  subrgpsr  16484  mvridlem  16485  mvrf  16490  mplmon  16528  mplmonmul  16529  mplcoe1  16530  mplcoe3  16531  mplcoe2  16532  mplbas2  16533  psrbagsn  16557  evlslem4  16566  evlslem2  16570  psropprmul  16634  coe1mul2  16664  coe1tmmul2  16670  coe1tmmul  16671  ply1coe  16686  gsumfsum  16768  expmhm  16778  expghm  16779  mulgghm2  16788  isphld  16887  pjff  16941  pptbas  17074  tgrest  17225  resttopon  17227  rest0  17235  restfpw  17245  ordtbaslem  17254  ordtuni  17256  ordtrest  17268  cnpfval  17300  pnrmopn  17409  cncmp  17457  discmp  17463  1stcfb  17510  2ndcomap  17523  dis2ndc  17525  lly1stc  17561  kgencmp  17579  ptpjpre1  17605  ptpjcn  17645  ptcldmpt  17648  ptclsg  17649  dfac14  17652  xkoccn  17653  txcnp  17654  ptcnp  17656  txcnmpt  17658  uptx  17659  ptcn  17661  ptrescn  17673  txlm  17682  xkoptsub  17688  xkoco1cn  17691  xkoco2cn  17692  cnmpt11  17697  xkoinjcn  17721  kqffn  17759  pt1hmeo  17840  fbasrn  17918  trfilss  17923  trfg  17925  rnelfmlem  17986  txflf  18040  flfcnp2  18041  fclscmpi  18063  alexsublem  18077  ptcmplem3  18087  symgtgp  18133  subgntr  18138  opnsubg  18139  clsnsg  18141  tgpconcomp  18144  tsmsfbas  18159  eltsms  18164  haustsms  18167  tsmscls  18169  tsms0  18173  tsmsmhm  18177  tgptsmscls  18181  tsmssplit  18183  tsmsxplem1  18184  tsmsxplem2  18185  ustuqtop0  18272  prdsdsf  18399  prdsxmetlem  18400  imasdsf1olem  18405  prdsbl  18523  stdbdxmet  18547  met1stc  18553  nmf2  18642  nmof  18755  xrge0gsumle  18866  xrge0tsms  18867  metdsf  18880  metdsge  18881  mulc1cncf  18937  cncfmpt2ss  18947  cnmptre  18954  evth  18986  evth2  18987  lebnumlem1  18988  cphnmf  19160  tchcph  19196  cmetcaulem  19243  minveclem1  19327  minveclem3b  19331  ovollb2lem  19386  ovolctb  19388  ovolunlem1a  19394  ovolunlem1  19395  ovoliunlem1  19400  ovoliunlem2  19401  ovoliun  19403  ovolshftlem1  19407  ovolscalem1  19411  ovolicc1  19414  iunmbl  19449  ioombl1lem1  19454  uniioombllem2  19477  uniioombllem3  19479  volsup2  19499  volcn  19500  vitalilem4  19505  vitalilem5  19506  mbfconst  19529  ismbfcn2  19533  mbfeqalem  19536  mbfss  19540  mbfmulc2re  19542  mbfmax  19543  mbfneg  19544  mbfpos  19545  mbfposr  19546  mbfposb  19547  mbfadd  19555  mbfmulc2  19557  mbfsup  19558  mbfinf  19559  mbflimsup  19560  mbflimlem  19561  mbflim  19562  i1f1lem  19583  i1f1  19584  i1fres  19599  itg1climres  19608  mbfi1fseqlem3  19611  mbfi1fseqlem4  19612  mbfi1flimlem  19616  mbfi1flim  19617  mbfmullem2  19618  mbfmul  19620  itg2const2  19635  itg2seq  19636  itg2splitlem  19642  itg2split  19643  itg2monolem1  19644  itg2monolem2  19645  itg2monolem3  19646  itg2mono  19647  itg2i1fseq  19649  itg2i1fseq2  19650  itg2gt0  19654  itg2cnlem1  19655  itg2cnlem2  19656  itg2cn  19657  isibl2  19660  iblss  19698  itgitg1  19702  itgle  19703  itgeqa  19707  itgss3  19708  ibladdlem  19713  itgaddlem1  19716  iblabslem  19721  iblabs  19722  iblabsr  19723  iblmulc2  19724  itgmulc2lem1  19725  bddmulibl  19732  itggt0  19735  itgcn  19736  ellimc2  19766  limcmpt  19772  limcres  19775  limccnp  19780  limccnp2  19781  limcco  19782  perfdvf  19792  dvreslem  19798  dvcnp2  19808  dvaddbr  19826  dvmulbr  19827  dvcjbr  19837  dvexp  19841  dvrec  19843  dvmptres3  19844  dvmptadd  19848  dvmptmul  19849  dvmptres2  19850  dvmptcmul  19852  dvmptcj  19856  dvmptntr  19859  dvmptco  19860  dvcnvlem  19862  dvef  19866  dvferm1  19871  dvferm2  19873  rolle  19876  dvlipcn  19880  dvle  19893  dvivthlem1  19894  dvivth  19896  lhop1lem  19899  lhop1  19900  lhop2  19901  lhop  19902  dvfsumle  19907  dvfsumge  19908  dvmptrecl  19910  dvfsumrlimf  19911  dvfsumlem2  19913  dvfsumlem3  19914  ftc1lem2  19922  ftc1lem6  19927  itgsubstlem  19934  evlslem6  19936  evlslem3  19937  evlslem1  19938  evlsval2  19943  tdeglem1  19983  tdeglem4  19985  coe1mul3  20024  elply2  20117  plyf  20119  elplyd  20123  plypf1  20133  coeeq2  20163  coemullem  20170  coe1termlem  20178  dvply2g  20204  elqaalem2  20239  taylfvallem  20276  taylf  20279  tayl0  20280  taylpfval  20283  taylpf  20284  taylthlem1  20291  taylthlem2  20292  ulmshftlem  20307  ulmshft  20308  ulmcau  20313  ulmss  20315  ulmdvlem1  20318  ulmdvlem3  20320  mtest  20322  mtestbdd  20323  iblulm  20325  itgulm2  20327  psergf  20330  radcnvlem1  20331  dvradcnv  20339  pserulm  20340  psercn2  20341  pserdvlem2  20346  abelthlem4  20352  abelthlem9  20358  pige3  20427  efif1olem4  20449  logtayl  20553  logccv  20556  loglesqr  20644  leibpi  20784  rlimcnp  20806  rlimcnp2  20807  xrlimcnp  20809  efrlim  20810  dfef2  20811  o1cxp  20815  cxp2lim  20817  amgmlem  20830  basellem2  20866  basellem4  20868  basellem7  20871  basellem9  20873  sqff1o  20967  fsumvma  20999  dchrelbasd  21025  lgsfcl2  21088  lgsqrlem2  21128  lgseisenlem1  21135  lgseisenlem3  21137  lgseisenlem4  21138  chpo1ub  21176  dchrisumlema  21184  dchrmusum2  21190  dchrvmasumiflem1  21197  dchrisum0ff  21203  dchrisum0lem1b  21211  dchrisum0lem2a  21213  logsqvma2  21239  pnt2  21309  pnt  21310  abvcxp  21311  padicabv  21326  nbgraf1olem2  21454  vdgrf  21671  vdgrfif  21672  efghgrp  21963  ipblnfi  22359  ubthlem1  22374  minvecolem1  22378  htthlem  22422  hlimadd  22697  chscllem1  23141  hoaddcl  23263  homulcl  23264  brafn  23452  kbop  23458  cnlnadjlem2  23573  strlem3a  23757  hstrlem3a  23765  off2  24056  xppreima2  24062  fmpt3d  24072  xrge0tsmsd  24225  xrge0mulc1cn  24329  esumf1o  24447  esumadd  24450  esumcst  24457  esumpfinval  24467  esumpcvgval  24470  esumcvg  24478  measinb  24577  measdivcst  24581  mbfmco2  24617  sitgclg  24658  dstfrvclim1  24737  lgamgulmlem2  24816  lgamgulmlem6  24820  lgamcvg2  24841  gamcvg  24842  regamcl  24847  relgamcl  24848  erdszelem9  24887  indispcon  24923  cvxpcon  24931  cvmsss2  24963  cvmliftlem6  24979  cvmliftlem8  24981  cvmlift3lem3  25010  divcnvlin  25214  prodfdiv  25226  prodrblem  25257  prodmolem2a  25262  fprodf1o  25274  prodss  25275  fprodss  25276  fprodser  25277  fprodcl2lem  25278  fprodmul  25286  fproddiv  25287  fprodefsum  25300  fprodn0  25305  iprodclim3  25315  iprodefisum  25320  faclimlem2  25365  faclim  25367  faclim2  25369  axlowdimlem15  25897  mblfinlem2  26246  volsupnfl  26253  mbfposadd  26256  itg2addnclem2  26259  itg2gt0cn  26262  ibladdnclem  26263  itgaddnclem1  26265  itgaddnc  26267  iblabsnclem  26270  iblabsnc  26271  iblmulc2nc  26272  itgmulc2nclem1  26273  itgmulc2nclem2  26274  itgmulc2nc  26275  itgabsnc  26276  bddiblnc  26277  itggt0cn  26279  ftc1cnnc  26281  ftc1anclem1  26282  ftc1anclem2  26283  ftc1anclem3  26284  ftc1anclem4  26285  ftc1anclem5  26286  ftc1anclem6  26287  ftc1anclem7  26288  ftc1anclem8  26289  ftc1anc  26290  areacirclem4  26297  comppfsc  26389  upixp  26433  totbndbnd  26500  prdsbnd  26504  cntotbnd  26507  rrnequiv  26546  cmpfiiin  26753  mzpclall  26786  mzpindd  26805  fphpdo  26880  dnnumch3  27124  kelac1  27140  dfac21  27143  pwssplit0  27166  frlmgsum  27211  uvcff  27219  uvcresum  27221  frlmsplit2  27222  frlmup1  27229  pmtrf  27376  psgnunilem5  27396  mamucl  27435  mamulid  27437  mamurid  27438  mamuass  27439  mamudi  27440  mamudir  27441  mamuvs1  27442  mamuvs2  27443  expgrowth  27531  expcnfg  27704  clim1fr1  27705  itgsinexplem1  27726  wlkiswwlk2lem5  28365  frgrancvvdeqlem5  28485  lsatlss  29856  lflnegcl  29935  lshpkrcl  29976  tendoplcl  31640  tendo0cl  31649  tendoicl  31655
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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 4332  ax-nul 4340  ax-pr 4405
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 4215  df-opab 4269  df-mpt 4270  df-id 4500  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-fv 5464
  Copyright terms: Public domain W3C validator