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

Theorem fmptd 5684
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 2626 . 2  |-  ( ph  ->  A. x  e.  A  B  e.  C )
3 fmptd.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43fmpt 5681 . 2  |-  ( A. x  e.  A  B  e.  C  <->  F : A --> C )
52, 4sylib 188 1  |-  ( ph  ->  F : A --> C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684   A.wral 2543    e. cmpt 4077   -->wf 5251
This theorem is referenced by:  fmptco  5691  fliftrel  5807  off  6093  caofinvl  6104  curry1f  6212  curry2f  6214  fnwelem  6230  fdiagfn  6811  resixpfo  6854  pw2f1olem  6966  mapxpen  7027  xpmapenlem  7028  unxpdomlem3  7069  wdom2d  7294  cantnfp1lem1  7380  cantnfp1lem2  7381  cantnfp1lem3  7382  cantnflem1d  7390  cantnflem1  7391  cantnf  7395  fseqenlem1  7651  fseqenlem2  7652  dfac8clem  7659  ac5num  7663  acni2  7673  infpwfien  7689  coftr  7899  fin23lem39  7976  isf34lem2  7999  fin1a2lem12  8037  axcc2lem  8062  axdc2lem  8074  axdc3lem4  8079  pwcfsdom  8205  canthp1lem2  8275  wuncval2  8369  gruf  8433  rpnnen1lem1  10342  monoord2  11077  seqf1o  11087  ccatcl  11429  swrdcl  11452  revcl  11479  revlen  11480  ello1mpt  11995  lo1o12  12007  lo1eq  12042  rlimeq  12043  climmpt2  12047  rlimcld2  12052  climrecl  12057  climge0  12058  o1compt  12061  rlimcn1b  12063  rlimcn2  12064  rlimdiv  12119  rlimsqzlem  12122  isercoll2  12142  caurcvg2  12150  caucvg  12151  sumrblem  12184  summolem2a  12188  fsumf1o  12196  sumss  12197  fsumss  12198  fsumcl2lem  12204  fsumadd  12211  isumclim3  12222  isummulc2  12225  fsummulc2  12246  fsumrelem  12265  climfsum  12278  isumshft  12298  divcnv  12312  supcvg  12314  rpnnen2lem2  12494  crt  12846  eulerthlem1  12849  iserodd  12888  prmreclem2  12964  prmreclem6  12968  1arithlem3  12972  4sqlem11  13002  vdwapf  13019  vdwlem2  13029  vdwlem4  13031  vdwlem6  13033  vdwlem10  13037  ramub1lem2  13074  ramcl  13076  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  mrcflem  13508  mreacs  13560  acsfn  13561  homaf  13862  prfcl  13977  curf1cl  14002  hofcllem  14032  hofcl  14033  yonedalem3a  14048  yonedalem4c  14051  yonedainv  14055  prdspjmhm  14443  pwsco1mhm  14446  pwsco2mhm  14447  gsumz  14458  gsumwspan  14468  vrmdfval  14478  vrmdf  14480  frmdup1  14486  grpinvf  14526  cycsubgcl  14643  cycsubgss  14644  conjghm  14713  conjnmz  14716  divsghm  14719  galactghm  14783  odf1  14875  dfod2  14877  odf1o2  14884  pgpssslw  14925  sylow2blem1  14931  pj1f  15006  frgpmhm  15074  vrgpf  15077  mulgmhm  15127  mulgghm  15128  iscyggen2  15168  cyggenod  15171  iscyg3  15173  gsumzsplit  15206  gsumsplit2  15208  gsumconst  15209  gsummhm2  15212  gsum2d  15223  prdsgsum  15229  dprdfeq0  15257  dprdlub  15261  dprdz  15265  dprd2dlem1  15276  dprd2da  15277  ablfac1b  15305  ablfac2  15324  rnglghm  15388  rngrghm  15389  gsumdixp  15392  abvtrivd  15605  issrngd  15626  lmodvsghm  15686  lspf  15731  asclf  16077  psrass1lem  16123  psrbas  16124  psrmulcllem  16132  psr1cl  16147  psrlidm  16148  psrridm  16149  psrass1  16150  psrdi  16151  psrdir  16152  psrcom  16153  resspsrmul  16161  subrgpsr  16163  mvridlem  16164  mvrf  16169  mplmon  16207  mplmonmul  16208  mplcoe1  16209  mplcoe3  16210  mplcoe2  16211  mplbas2  16212  psrbagsn  16236  evlslem4  16245  evlslem2  16249  psropprmul  16316  coe1mul2  16346  coe1tmmul2  16352  coe1tmmul  16353  ply1coe  16368  gsumfsum  16439  expmhm  16449  expghm  16450  mulgghm2  16459  isphld  16558  pjff  16612  pptbas  16745  tgrest  16890  resttopon  16892  rest0  16900  restfpw  16910  ordtbaslem  16918  ordtuni  16920  ordtrest  16932  cnpfval  16964  pnrmopn  17071  cncmp  17119  discmp  17125  1stcfb  17171  2ndcomap  17184  dis2ndc  17186  lly1stc  17222  kgencmp  17240  ptpjpre1  17266  ptpjcn  17305  ptcldmpt  17308  ptclsg  17309  dfac14  17312  xkoccn  17313  txcnp  17314  ptcnp  17316  txcnmpt  17318  uptx  17319  ptcn  17321  ptrescn  17333  txlm  17342  xkoptsub  17348  xkoco1cn  17351  xkoco2cn  17352  cnmpt11  17357  xkoinjcn  17381  kqffn  17416  pt1hmeo  17497  fbasrn  17579  trfilss  17584  trfg  17586  rnelfmlem  17647  txflf  17701  flfcnp2  17702  fclscmpi  17724  alexsublem  17738  ptcmplem3  17748  symgtgp  17784  subgntr  17789  opnsubg  17790  clsnsg  17792  tgpconcomp  17795  tsmsfbas  17810  eltsms  17815  haustsms  17818  tsmscls  17820  tsms0  17824  tsmsmhm  17828  tgptsmscls  17832  tsmssplit  17834  tsmsxplem1  17835  tsmsxplem2  17836  prdsdsf  17931  prdsxmetlem  17932  imasdsf1olem  17937  prdsbl  18037  stdbdxmet  18061  met1stc  18067  nmf2  18115  nmof  18228  xrge0gsumle  18338  xrge0tsms  18339  metdsf  18352  metdsge  18353  mulc1cncf  18409  cncfmpt2ss  18419  cnmptre  18425  evth  18457  evth2  18458  lebnumlem1  18459  cphnmf  18631  tchcph  18667  cmetcaulem  18714  minveclem1  18788  minveclem3b  18792  ovollb2lem  18847  ovolctb  18849  ovolunlem1a  18855  ovolunlem1  18856  ovoliunlem1  18861  ovoliunlem2  18862  ovoliun  18864  ovolshftlem1  18868  ovolscalem1  18872  ovolicc1  18875  iunmbl  18910  ioombl1lem1  18915  uniioombllem2  18938  uniioombllem3  18940  volsup2  18960  volcn  18961  vitalilem4  18966  vitalilem5  18967  mbfconst  18990  ismbfcn2  18994  mbfeqalem  18997  mbfss  19001  mbfmulc2re  19003  mbfmax  19004  mbfneg  19005  mbfpos  19006  mbfposr  19007  mbfposb  19008  mbfadd  19016  mbfmulc2  19018  mbfsup  19019  mbfinf  19020  mbflimsup  19021  mbflimlem  19022  mbflim  19023  i1f1lem  19044  i1f1  19045  i1fres  19060  itg1climres  19069  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  mbfi1flimlem  19077  mbfi1flim  19078  mbfmullem2  19079  mbfmul  19081  itg2const2  19096  itg2seq  19097  itg2splitlem  19103  itg2split  19104  itg2monolem1  19105  itg2monolem2  19106  itg2monolem3  19107  itg2mono  19108  itg2i1fseq  19110  itg2i1fseq2  19111  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  itg2cn  19118  isibl2  19121  iblss  19159  itgitg1  19163  itgle  19164  itgeqa  19168  itgss3  19169  ibladdlem  19174  itgaddlem1  19177  iblabslem  19182  iblabs  19183  iblabsr  19184  iblmulc2  19185  itgmulc2lem1  19186  bddmulibl  19193  itggt0  19196  itgcn  19197  ellimc2  19227  limcmpt  19233  limcres  19236  limccnp  19241  limccnp2  19242  limcco  19243  perfdvf  19253  dvreslem  19259  dvcnp2  19269  dvaddbr  19287  dvmulbr  19288  dvcjbr  19298  dvexp  19302  dvrec  19304  dvmptres3  19305  dvmptadd  19309  dvmptmul  19310  dvmptres2  19311  dvmptcmul  19313  dvmptcj  19317  dvmptntr  19320  dvmptco  19321  dvcnvlem  19323  dvef  19327  dvferm1  19332  dvferm2  19334  rolle  19337  dvlipcn  19341  dvle  19354  dvivthlem1  19355  dvivth  19357  lhop1lem  19360  lhop1  19361  lhop2  19362  lhop  19363  dvfsumle  19368  dvfsumge  19369  dvmptrecl  19371  dvfsumrlimf  19372  dvfsumlem2  19374  dvfsumlem3  19375  ftc1lem2  19383  ftc1lem6  19388  itgsubstlem  19395  evlslem6  19397  evlslem3  19398  evlslem1  19399  evlsval2  19404  tdeglem1  19444  tdeglem4  19446  coe1mul3  19485  elply2  19578  plyf  19580  elplyd  19584  plypf1  19594  coeeq2  19624  coemullem  19631  coe1termlem  19639  dvply2g  19665  elqaalem2  19700  taylfvallem  19737  taylf  19740  tayl0  19741  taylpfval  19744  taylpf  19745  taylthlem1  19752  taylthlem2  19753  ulmshftlem  19768  ulmshft  19769  ulmcau  19772  ulmss  19774  ulmdvlem1  19777  ulmdvlem3  19779  mtest  19781  iblulm  19783  itgulm2  19785  psergf  19788  radcnvlem1  19789  dvradcnv  19797  pserulm  19798  psercn2  19799  pserdvlem2  19804  abelthlem4  19810  abelthlem9  19816  pige3  19885  efif1olem4  19907  logtayl  20007  logccv  20010  loglesqr  20098  leibpi  20238  rlimcnp  20260  rlimcnp2  20261  xrlimcnp  20263  efrlim  20264  dfef2  20265  o1cxp  20269  cxp2lim  20271  amgmlem  20284  basellem2  20319  basellem4  20321  basellem7  20324  basellem9  20326  sqff1o  20420  fsumvma  20452  dchrelbasd  20478  lgsfcl2  20541  lgsqrlem2  20581  lgseisenlem1  20588  lgseisenlem3  20590  lgseisenlem4  20591  chpo1ub  20629  dchrisumlema  20637  dchrmusum2  20643  dchrvmasumiflem1  20650  dchrisum0ff  20656  dchrisum0lem1b  20664  dchrisum0lem2a  20666  logsqvma2  20692  pnt2  20762  pnt  20763  abvcxp  20764  padicabv  20779  efghgrp  21040  ipblnfi  21434  ubthlem1  21449  minvecolem1  21453  htthlem  21497  hlimadd  21772  chscllem1  22216  hoaddcl  22338  homulcl  22339  brafn  22527  kbop  22533  cnlnadjlem2  22648  strlem3a  22832  hstrlem3a  22840  off2  23208  xrge0tsmsd  23382  esumf1o  23429  esumadd  23432  esumpcvgval  23446  esumcvg  23454  ofcf  23464  measinb  23548  mbfmcst  23564  dstfrvclim1  23678  erdszelem9  23730  indispcon  23765  cvxpcon  23773  cvmsss2  23805  cvmliftlem6  23821  cvmliftlem8  23823  cvmlift3lem3  23852  vdgrf  23891  axlowdimlem15  24584  areacirclem3  24926  areacirclem5  24929  prmapcp2  25157  prjmapcp  25165  claddrv  25647  zernpl  25653  addassv  25656  cnegvex2  25660  rnegvex2  25661  domcatfun  25925  codcatfun  25934  idcatfun  25941  clscnc  26010  comppfsc  26307  upixp  26403  totbndbnd  26513  prdsbnd  26517  cntotbnd  26520  rrnequiv  26559  cmpfiiin  26772  mzpclall  26805  mzpindd  26824  fphpdo  26900  dnnumch3  27144  kelac1  27161  dfac21  27164  pwssplit0  27187  frlmgsum  27232  uvcff  27240  uvcresum  27242  frlmsplit2  27243  frlmup1  27250  pmtrf  27397  psgnunilem5  27417  mamucl  27456  mamulid  27458  mamurid  27459  mamuass  27460  mamudi  27461  mamudir  27462  mamuvs1  27463  mamuvs2  27464  expgrowth  27552  expcnfg  27726  itgsinexplem1  27748  lsatlss  29186  lflnegcl  29265  lshpkrcl  29306  tendoplcl  30970  tendo0cl  30979  tendoicl  30985
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-fv 5263
  Copyright terms: Public domain W3C validator