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

Theorem fmptd 5966
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 2822 . 2  |-  ( ph  ->  A. x  e.  A  B  e.  C )
3 fmptd.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43fmpt 5963 . 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 1370    e. wcel 1758   A.wral 2795    |-> cmpt 4448   -->wf 5512
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-fv 5524
This theorem is referenced by:  fmptco  5975  fliftrel  6100  off  6434  caofinvl  6447  curry1f  6766  curry2f  6768  fnwelem  6787  fdiagfn  7356  resixpfo  7401  pw2f1olem  7515  mapxpen  7577  xpmapenlem  7578  unxpdomlem3  7620  fsuppmptdm  7732  fsuppmptif  7750  wdom2d  7896  cantnfp1lem1  7987  cantnfp1lem2  7988  cantnfp1lem3  7989  cantnflem1d  7997  cantnflem1  7998  cantnf  8002  cantnfp1lem1OLD  8013  cantnfp1lem2OLD  8014  cantnfp1lem3OLD  8015  cantnflem1dOLD  8020  cantnflem1OLD  8021  cantnfOLD  8024  fseqenlem1  8295  fseqenlem2  8296  dfac8clem  8303  ac5num  8307  acni2  8317  infpwfien  8333  coftr  8543  fin23lem39  8620  isf34lem2  8643  fin1a2lem12  8681  axcc2lem  8706  axdc2lem  8718  axdc3lem4  8723  pwcfsdom  8848  canthp1lem2  8921  wuncval2  9015  gruf  9079  rpnnen1lem1  11080  monoord2  11938  seqf1o  11948  ccatcl  12376  swrdcl  12417  revcl  12503  revlen  12504  ello1mpt  13101  lo1o12  13113  lo1eq  13148  rlimeq  13149  climmpt2  13153  rlimcld2  13158  climrecl  13163  climge0  13164  o1compt  13167  rlimcn1b  13169  rlimcn2  13170  rlimdiv  13225  rlimsqzlem  13228  isercoll2  13248  caurcvg2  13257  caucvg  13258  sumrblem  13290  summolem2a  13294  fsumf1o  13302  sumss  13303  fsumss  13304  fsumcl2lem  13310  fsumadd  13317  isumclim3  13328  isummulc2  13331  fsummulc2  13353  fsumrelem  13372  climfsum  13385  isumshft  13404  divcnv  13418  supcvg  13420  rpnnen2lem2  13600  crt  13955  eulerthlem1  13958  iserodd  14004  prmreclem2  14080  prmreclem6  14084  1arithlem3  14088  4sqlem11  14118  vdwapf  14135  vdwlem2  14145  vdwlem4  14147  vdwlem6  14149  vdwlem10  14153  ramub1lem2  14190  ramcl  14192  prdsplusg  14498  prdsmulr  14499  prdsvsca  14500  mrcflem  14646  mreacs  14698  acsfn  14699  homaf  15000  prfcl  15115  curf1cl  15140  hofcllem  15170  hofcl  15171  yonedalem3a  15186  yonedalem4c  15189  yonedainv  15193  prdspjmhm  15597  pwsco1mhm  15600  pwsco2mhm  15601  gsumz  15613  gsumwspan  15626  vrmdfval  15636  vrmdf  15638  frmdup1  15644  grpinvf  15684  cycsubgcl  15809  cycsubgss  15810  conjghm  15879  conjnmz  15882  divsghm  15885  galactghm  16010  symgextf  16024  symgfixf  16044  pmtrf  16063  psgnunilem5  16102  odf1  16167  dfod2  16169  odf1o2  16176  pgpssslw  16217  sylow2blem1  16223  pj1f  16298  frgpmhm  16366  vrgpf  16369  mulgmhm  16419  mulgghm  16420  iscyggen2  16462  cyggenod  16465  iscyg3  16467  gsummptfsadd  16518  gsummptfsaddOLD  16519  gsumzsplit  16522  gsumzsplitOLD  16523  gsumsplit2  16526  gsumsplit2OLD  16527  gsummptfidmsplitres  16529  gsumconst  16532  gsummptshft  16534  gsummhm2  16539  gsummhm2OLD  16540  gsummptmhm  16541  gsummptfidminv  16550  gsumzunsnd  16556  gsummpt1n0  16561  gsum2dlem1  16566  gsum2dlem2  16567  gsum2d  16568  gsum2dOLD  16569  prdsgsum  16576  prdsgsumOLD  16577  dprdfeq0  16617  dprdfeq0OLD  16624  dprdlub  16628  dprdz  16632  dprd2dlem1  16645  dprd2da  16646  ablfac1b  16676  ablfac2  16695  srglmhm  16739  srgrmhm  16740  rnglghm  16799  rngrghm  16800  gsumdixpOLD  16806  gsumdixp  16807  abvtrivd  17031  issrngd  17052  lmodvsghm  17112  lspf  17161  pwssplit0  17245  asclf  17514  snifpsrbag  17539  psrass1lem  17553  psrbasOLD  17555  psrmulcllem  17564  psr1cl  17579  psrlidm  17580  psrlidmOLD  17581  psrridm  17582  psrridmOLD  17583  psrdi  17585  psrdir  17586  psrcom  17588  resspsrmul  17596  subrgpsr  17598  mvridlemOLD  17599  mvrf  17604  mplmon  17649  mplmonmul  17650  mplcoe1  17651  mplcoe3OLD  17653  mplcoe5lem  17654  mplcoe5  17655  mplcoe2OLD  17657  mplbas2  17658  mplbas2OLD  17659  psrbagsn  17684  evlslem4OLD  17697  evlslem4  17698  evlslem2  17704  evlslem6  17705  evlslem6OLD  17706  evlslem3  17707  evlslem1  17708  evlsval2  17713  psropprmul  17800  coe1mul2  17830  coe1tmmul2  17837  coe1tmmul  17838  ply1coe  17855  ply1coeOLD  17856  gsumfsum  17988  expmhm  17989  expghm  18032  expghmOLD  18033  mulgghm2  18034  mulgghm2OLD  18037  evpmodpmf1o  18135  isphld  18192  pjff  18246  frlmgsumOLD  18304  frlmgsum  18305  frlmsplit2  18306  frlmphl  18315  uvcff  18325  uvcresum  18327  frlmup1  18335  mamulid  18413  mamurid  18414  mdetf  18517  mdetunilem9  18542  mdetuni0  18543  mdetmul  18545  maduf  18563  pptbas  18728  tgrest  18879  resttopon  18881  rest0  18889  restfpw  18899  ordtbaslem  18908  ordtuni  18910  ordtrest  18922  cnpfval  18954  pnrmopn  19063  cncmp  19111  discmp  19117  1stcfb  19165  2ndcomap  19178  dis2ndc  19180  lly1stc  19216  kgencmp  19234  ptpjpre1  19260  ptpjcn  19300  ptcldmpt  19303  ptclsg  19304  dfac14  19307  xkoccn  19308  txcnp  19309  ptcnp  19311  txcnmpt  19313  uptx  19314  ptcn  19316  ptrescn  19328  txlm  19337  xkoptsub  19343  xkoco1cn  19346  xkoco2cn  19347  cnmpt11  19352  xkoinjcn  19376  kqffn  19414  pt1hmeo  19495  fbasrn  19573  trfilss  19578  trfg  19580  rnelfmlem  19641  txflf  19695  flfcnp2  19696  fclscmpi  19718  alexsublem  19732  ptcmplem3  19742  symgtgp  19788  subgntr  19793  opnsubg  19794  clsnsg  19796  tgpconcomp  19799  tsmsfbas  19814  eltsms  19819  haustsms  19822  tsmscls  19824  tsms0  19831  tsmsmhm  19836  tgptsmscls  19840  tsmssplit  19842  tsmsxplem1  19843  tsmsxplem2  19844  ustuqtop0  19931  prdsdsf  20058  prdsxmetlem  20059  imasdsf1olem  20064  prdsbl  20182  stdbdxmet  20206  met1stc  20212  nmf2  20301  nmof  20414  xrge0gsumle  20526  xrge0tsms  20527  metdsf  20540  metdsge  20541  mulc1cncf  20597  cncfmpt2ss  20607  cnmptre  20615  evth  20647  evth2  20648  lebnumlem1  20649  cphnmf  20830  tchcph  20868  cmetcaulem  20915  rrxmval  21020  minveclem1  21027  minveclem3b  21031  ovollb2lem  21087  ovolctb  21089  ovolunlem1a  21095  ovolunlem1  21096  ovoliunlem1  21101  ovoliunlem2  21102  ovoliun  21104  ovolshftlem1  21108  ovolscalem1  21112  ovolicc1  21115  iunmbl  21150  ioombl1lem1  21155  uniioombllem2  21179  uniioombllem3  21181  volsup2  21201  volcn  21202  vitalilem4  21207  vitalilem5  21208  mbfconst  21229  ismbfcn2  21233  mbfeqalem  21236  mbfss  21240  mbfmulc2re  21242  mbfmax  21243  mbfneg  21244  mbfpos  21245  mbfposr  21246  mbfposb  21247  mbfadd  21255  mbfmulc2  21257  mbfsup  21258  mbfinf  21259  mbflimsup  21260  mbflimlem  21261  mbflim  21262  i1f1lem  21283  i1f1  21284  i1fres  21299  itg1climres  21308  mbfi1fseqlem3  21311  mbfi1fseqlem4  21312  mbfi1flimlem  21316  mbfi1flim  21317  mbfmullem2  21318  mbfmul  21320  itg2const2  21335  itg2seq  21336  itg2splitlem  21342  itg2split  21343  itg2monolem1  21344  itg2monolem2  21345  itg2monolem3  21346  itg2mono  21347  itg2i1fseq  21349  itg2i1fseq2  21350  itg2gt0  21354  itg2cnlem1  21355  itg2cnlem2  21356  itg2cn  21357  isibl2  21360  iblss  21398  itgitg1  21402  itgle  21403  itgeqa  21407  itgss3  21408  ibladdlem  21413  itgaddlem1  21416  iblabslem  21421  iblabs  21422  iblabsr  21423  iblmulc2  21424  itgmulc2lem1  21425  bddmulibl  21432  itggt0  21435  itgcn  21436  ellimc2  21468  limcmpt  21474  limcres  21477  limccnp  21482  limccnp2  21483  limcco  21484  perfdvf  21494  dvreslem  21500  dvcnp2  21510  dvaddbr  21528  dvmulbr  21529  dvcjbr  21539  dvexp  21543  dvrec  21545  dvmptres3  21546  dvmptadd  21550  dvmptmul  21551  dvmptres2  21552  dvmptcmul  21554  dvmptcj  21558  dvmptntr  21561  dvmptco  21562  dvcnvlem  21564  dvef  21568  dvferm1  21573  dvferm2  21575  rolle  21578  dvlipcn  21582  dvle  21595  dvivthlem1  21596  dvivth  21598  lhop1lem  21601  lhop1  21602  lhop2  21603  lhop  21604  dvfsumle  21609  dvfsumge  21610  dvmptrecl  21612  dvfsumrlimf  21613  dvfsumlem2  21615  dvfsumlem3  21616  ftc1lem2  21624  ftc1lem6  21629  itgsubstlem  21636  tdeglem1  21643  tdeglem4  21645  coe1mul3  21687  elply2  21780  plyf  21782  elplyd  21786  plypf1  21796  coeeq2  21826  coemullem  21833  coe1termlem  21841  dvply2g  21867  elqaalem2  21902  taylfvallem  21939  taylf  21942  tayl0  21943  taylpfval  21946  taylpf  21947  taylthlem1  21954  taylthlem2  21955  ulmshftlem  21970  ulmshft  21971  ulmcau  21976  ulmss  21978  ulmdvlem1  21981  ulmdvlem3  21983  mtest  21985  mtestbdd  21986  iblulm  21988  itgulm2  21990  psergf  21993  radcnvlem1  21994  dvradcnv  22002  pserulm  22003  psercn2  22004  pserdvlem2  22009  abelthlem4  22015  abelthlem9  22021  pige3  22095  efif1olem4  22117  logtayl  22221  logccv  22224  loglesqr  22312  leibpi  22453  rlimcnp  22475  rlimcnp2  22476  xrlimcnp  22478  efrlim  22479  dfef2  22480  o1cxp  22484  cxp2lim  22486  amgmlem  22499  basellem2  22535  basellem4  22537  basellem7  22540  basellem9  22542  sqff1o  22636  fsumvma  22668  dchrelbasd  22694  lgsfcl2  22757  lgsqrlem2  22797  lgseisenlem1  22804  lgseisenlem3  22806  lgseisenlem4  22807  chpo1ub  22845  dchrisumlema  22853  dchrmusum2  22859  dchrvmasumiflem1  22866  dchrisum0ff  22872  dchrisum0lem1b  22880  dchrisum0lem2a  22882  logsqvma2  22908  pnt2  22978  pnt  22979  abvcxp  22980  padicabv  22995  axlowdimlem15  23337  nbgraf1olem2  23486  vdgrf  23703  vdgrfif  23704  efghgrp  23995  ipblnfi  24391  ubthlem1  24406  minvecolem1  24410  htthlem  24454  hlimadd  24730  chscllem1  25175  hoaddcl  25297  homulcl  25298  brafn  25486  kbop  25492  cnlnadjlem2  25607  strlem3a  25791  hstrlem3a  25799  off2  26093  xppreima2  26099  fmpt3d  26107  fpwrelmap  26167  gsummptf1o  26381  gsummptun  26382  regsumfsum  26384  gsumvsca1  26385  gsumvsca2  26386  xrge0tsmsd  26387  ordtrestNEW  26485  xrge0mulc1cn  26505  esumf1o  26638  esumadd  26641  esumcst  26648  esumpfinval  26658  esumpcvgval  26661  esumcvg  26669  measinb  26769  measdivcst  26773  mbfmco2  26814  sitgclg  26862  eulerpartlems  26877  dstfrvclim1  26994  gsumncl  27070  gsumnunsn  27071  signstf  27101  lgamgulmlem2  27150  lgamgulmlem6  27154  lgamcvg2  27175  gamcvg  27176  regamcl  27181  relgamcl  27182  erdszelem9  27221  indispcon  27257  cvxpcon  27265  cvmsss2  27297  cvmliftlem6  27313  cvmliftlem8  27315  cvmlift3lem3  27344  divcnvlin  27533  prodfdiv  27545  prodrblem  27576  prodmolem2a  27581  fprodf1o  27593  prodss  27594  fprodss  27595  fprodser  27596  fprodcl2lem  27597  fprodmul  27605  fproddiv  27606  fprodefsum  27619  fprodn0  27624  iprodclim3  27634  iprodefisum  27639  faclimlem2  27684  faclim  27686  faclim2  27688  finixpnum  28552  ptrest  28563  mblfinlem2  28567  volsupnfl  28574  mbfposadd  28577  itg2addnclem2  28582  itg2gt0cn  28585  ibladdnclem  28586  itgaddnclem1  28588  itgaddnc  28590  iblabsnclem  28593  iblabsnc  28594  iblmulc2nc  28595  itgmulc2nclem1  28596  itgmulc2nclem2  28597  itgmulc2nc  28598  itgabsnc  28599  bddiblnc  28600  itggt0cn  28602  ftc1cnnc  28604  ftc1anclem1  28605  ftc1anclem2  28606  ftc1anclem3  28607  ftc1anclem4  28608  ftc1anclem5  28609  ftc1anclem6  28610  ftc1anclem7  28611  ftc1anclem8  28612  ftc1anc  28613  areacirclem4  28625  comppfsc  28717  upixp  28761  totbndbnd  28826  prdsbnd  28830  cntotbnd  28833  rrnequiv  28872  cmpfiiin  29171  mzpclall  29201  mzpindd  29220  fphpdo  29294  dnnumch3  29538  kelac1  29554  dfac21  29557  itgpowd  29728  expgrowth  29747  expcnfg  29911  clim1fr1  29912  itgsinexplem1  29932  wlkiswwlk2lem5  30467  wlknwwlknfun  30480  wlkiswwlkfun  30487  wwlkextfun  30499  clwlkisclwwlklem2a  30585  clwwlkf  30594  clwlkfclwwlk  30655  frgrancvvdeqlem5  30765  numclwlk1lem2f  30823  numclwlk2lem2f  30834  gsummptfssub  30942  gsumlsscl  30958  gsumsmonply1  30984  gsummoncoe1  30985  ply1mulgsum  30990  lincfsuppcl  31054  linccl  31055  lincvalsc0  31062  lcoc0  31063  linc0scn0  31064  linc1  31066  lincsum  31070  lincscm  31071  lincscmcl  31073  lcoss  31077  lincext1  31095  el0ldep  31107  lincresunit1  31118  lincresunit3  31122  lmod1zr  31142  m2cpmfo  31215  m2cpminvf  31220  pmatcollpw1  31232  pmatcollpw4  31240  pmatcollpw4fi  31241  pmatcollpw4fi1lem1  31242  pmatcollpw4fi1lem2  31243  mply1topmatcl  31252  pmattomply1rn  31257  mp2pm2mplem2  31262  mp2pm2mp  31266  pmattomply1mhmlem2  31274  chfacfisf  31308  chfacfisfcpmat  31309  cpmidpmatlem2  31325  cpmadumatpolylem1  31335  cpmadumatpolylem3  31337  chcoeffeqlem  31340  cayhamlem4  31343  lsatlss  32947  lflnegcl  33026  lshpkrcl  33067  tendoplcl  34731  tendo0cl  34740  tendoicl  34746
  Copyright terms: Public domain W3C validator