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

Theorem fmptd 5862
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 2794 . 2  |-  ( ph  ->  A. x  e.  A  B  e.  C )
3 fmptd.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43fmpt 5859 . 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 1369    e. wcel 1756   A.wral 2710    e. cmpt 4345   -->wf 5409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421
This theorem is referenced by:  fmptco  5871  fliftrel  5996  off  6329  caofinvl  6342  curry1f  6661  curry2f  6663  fnwelem  6682  fdiagfn  7248  resixpfo  7293  pw2f1olem  7407  mapxpen  7469  xpmapenlem  7470  unxpdomlem3  7511  fsuppmptdm  7623  fsuppmptif  7641  wdom2d  7787  cantnfp1lem1  7878  cantnfp1lem2  7879  cantnfp1lem3  7880  cantnflem1d  7888  cantnflem1  7889  cantnf  7893  cantnfp1lem1OLD  7904  cantnfp1lem2OLD  7905  cantnfp1lem3OLD  7906  cantnflem1dOLD  7911  cantnflem1OLD  7912  cantnfOLD  7915  fseqenlem1  8186  fseqenlem2  8187  dfac8clem  8194  ac5num  8198  acni2  8208  infpwfien  8224  coftr  8434  fin23lem39  8511  isf34lem2  8534  fin1a2lem12  8572  axcc2lem  8597  axdc2lem  8609  axdc3lem4  8614  pwcfsdom  8739  canthp1lem2  8812  wuncval2  8906  gruf  8970  rpnnen1lem1  10971  monoord2  11829  seqf1o  11839  ccatcl  12266  swrdcl  12307  revcl  12393  revlen  12394  ello1mpt  12991  lo1o12  13003  lo1eq  13038  rlimeq  13039  climmpt2  13043  rlimcld2  13048  climrecl  13053  climge0  13054  o1compt  13057  rlimcn1b  13059  rlimcn2  13060  rlimdiv  13115  rlimsqzlem  13118  isercoll2  13138  caurcvg2  13147  caucvg  13148  sumrblem  13180  summolem2a  13184  fsumf1o  13192  sumss  13193  fsumss  13194  fsumcl2lem  13200  fsumadd  13207  isumclim3  13218  isummulc2  13221  fsummulc2  13243  fsumrelem  13262  climfsum  13275  isumshft  13294  divcnv  13308  supcvg  13310  rpnnen2lem2  13490  crt  13845  eulerthlem1  13848  iserodd  13894  prmreclem2  13970  prmreclem6  13974  1arithlem3  13978  4sqlem11  14008  vdwapf  14025  vdwlem2  14035  vdwlem4  14037  vdwlem6  14039  vdwlem10  14043  ramub1lem2  14080  ramcl  14082  prdsplusg  14388  prdsmulr  14389  prdsvsca  14390  mrcflem  14536  mreacs  14588  acsfn  14589  homaf  14890  prfcl  15005  curf1cl  15030  hofcllem  15060  hofcl  15061  yonedalem3a  15076  yonedalem4c  15079  yonedainv  15083  prdspjmhm  15486  pwsco1mhm  15489  pwsco2mhm  15490  gsumz  15502  gsumwspan  15515  vrmdfval  15525  vrmdf  15527  frmdup1  15533  grpinvf  15573  cycsubgcl  15698  cycsubgss  15699  conjghm  15768  conjnmz  15771  divsghm  15774  galactghm  15899  symgextf  15913  symgfixf  15933  pmtrf  15952  psgnunilem5  15991  odf1  16054  dfod2  16056  odf1o2  16063  pgpssslw  16104  sylow2blem1  16110  pj1f  16185  frgpmhm  16253  vrgpf  16256  mulgmhm  16306  mulgghm  16307  iscyggen2  16349  cyggenod  16352  iscyg3  16354  gsummptfsadd  16405  gsummptfsaddOLD  16406  gsumzsplit  16409  gsumzsplitOLD  16410  gsumsplit2  16413  gsumsplit2OLD  16414  gsummptfidmsplitres  16416  gsumconst  16417  gsummptshft  16419  gsummhm2  16424  gsummhm2OLD  16425  gsummptmhm  16426  gsummptfidminv  16435  gsummptif1n0  16445  gsum2dlem1  16449  gsum2dlem2  16450  gsum2d  16451  gsum2dOLD  16452  prdsgsum  16459  prdsgsumOLD  16460  dprdfeq0  16500  dprdfeq0OLD  16507  dprdlub  16511  dprdz  16515  dprd2dlem1  16528  dprd2da  16529  ablfac1b  16559  ablfac2  16578  srglmhm  16622  srgrmhm  16623  rnglghm  16681  rngrghm  16682  gsumdixpOLD  16688  gsumdixp  16689  abvtrivd  16903  issrngd  16924  lmodvsghm  16984  lspf  17032  pwssplit0  17116  asclf  17385  snifpsrbag  17410  psrass1lem  17424  psrbasOLD  17426  psrmulcllem  17435  psr1cl  17450  psrlidm  17451  psrlidmOLD  17452  psrridm  17453  psrridmOLD  17454  psrdi  17456  psrdir  17457  psrcom  17458  resspsrmul  17466  subrgpsr  17468  mvridlemOLD  17469  mvrf  17474  mplmon  17519  mplmonmul  17520  mplcoe1  17521  mplcoe3OLD  17523  mplcoe2  17524  mplcoe2OLD  17525  mplbas2  17526  mplbas2OLD  17527  psrbagsn  17552  evlslem4OLD  17565  evlslem4  17566  evlslem2  17572  evlslem6  17573  evlslem6OLD  17574  evlslem3  17575  evlslem1  17576  evlsval2  17581  psropprmul  17668  coe1mul2  17698  coe1tmmul2  17704  coe1tmmul  17705  ply1coe  17721  ply1coeOLD  17722  gsumfsum  17854  expmhm  17855  expghm  17898  expghmOLD  17899  mulgghm2  17900  mulgghm2OLD  17903  evpmodpmf1o  18001  isphld  18058  pjff  18112  frlmgsumOLD  18170  frlmgsum  18171  frlmsplit2  18172  frlmphl  18181  uvcff  18191  uvcresum  18193  frlmup1  18201  mamulid  18279  mamurid  18280  mdetf  18381  mdetunilem9  18401  mdetuni0  18402  mdetmul  18404  maduf  18422  pptbas  18587  tgrest  18738  resttopon  18740  rest0  18748  restfpw  18758  ordtbaslem  18767  ordtuni  18769  ordtrest  18781  cnpfval  18813  pnrmopn  18922  cncmp  18970  discmp  18976  1stcfb  19024  2ndcomap  19037  dis2ndc  19039  lly1stc  19075  kgencmp  19093  ptpjpre1  19119  ptpjcn  19159  ptcldmpt  19162  ptclsg  19163  dfac14  19166  xkoccn  19167  txcnp  19168  ptcnp  19170  txcnmpt  19172  uptx  19173  ptcn  19175  ptrescn  19187  txlm  19196  xkoptsub  19202  xkoco1cn  19205  xkoco2cn  19206  cnmpt11  19211  xkoinjcn  19235  kqffn  19273  pt1hmeo  19354  fbasrn  19432  trfilss  19437  trfg  19439  rnelfmlem  19500  txflf  19554  flfcnp2  19555  fclscmpi  19577  alexsublem  19591  ptcmplem3  19601  symgtgp  19647  subgntr  19652  opnsubg  19653  clsnsg  19655  tgpconcomp  19658  tsmsfbas  19673  eltsms  19678  haustsms  19681  tsmscls  19683  tsms0  19690  tsmsmhm  19695  tgptsmscls  19699  tsmssplit  19701  tsmsxplem1  19702  tsmsxplem2  19703  ustuqtop0  19790  prdsdsf  19917  prdsxmetlem  19918  imasdsf1olem  19923  prdsbl  20041  stdbdxmet  20065  met1stc  20071  nmf2  20160  nmof  20273  xrge0gsumle  20385  xrge0tsms  20386  metdsf  20399  metdsge  20400  mulc1cncf  20456  cncfmpt2ss  20466  cnmptre  20474  evth  20506  evth2  20507  lebnumlem1  20508  cphnmf  20689  tchcph  20727  cmetcaulem  20774  rrxmval  20879  minveclem1  20886  minveclem3b  20890  ovollb2lem  20946  ovolctb  20948  ovolunlem1a  20954  ovolunlem1  20955  ovoliunlem1  20960  ovoliunlem2  20961  ovoliun  20963  ovolshftlem1  20967  ovolscalem1  20971  ovolicc1  20974  iunmbl  21009  ioombl1lem1  21014  uniioombllem2  21038  uniioombllem3  21040  volsup2  21060  volcn  21061  vitalilem4  21066  vitalilem5  21067  mbfconst  21088  ismbfcn2  21092  mbfeqalem  21095  mbfss  21099  mbfmulc2re  21101  mbfmax  21102  mbfneg  21103  mbfpos  21104  mbfposr  21105  mbfposb  21106  mbfadd  21114  mbfmulc2  21116  mbfsup  21117  mbfinf  21118  mbflimsup  21119  mbflimlem  21120  mbflim  21121  i1f1lem  21142  i1f1  21143  i1fres  21158  itg1climres  21167  mbfi1fseqlem3  21170  mbfi1fseqlem4  21171  mbfi1flimlem  21175  mbfi1flim  21176  mbfmullem2  21177  mbfmul  21179  itg2const2  21194  itg2seq  21195  itg2splitlem  21201  itg2split  21202  itg2monolem1  21203  itg2monolem2  21204  itg2monolem3  21205  itg2mono  21206  itg2i1fseq  21208  itg2i1fseq2  21209  itg2gt0  21213  itg2cnlem1  21214  itg2cnlem2  21215  itg2cn  21216  isibl2  21219  iblss  21257  itgitg1  21261  itgle  21262  itgeqa  21266  itgss3  21267  ibladdlem  21272  itgaddlem1  21275  iblabslem  21280  iblabs  21281  iblabsr  21282  iblmulc2  21283  itgmulc2lem1  21284  bddmulibl  21291  itggt0  21294  itgcn  21295  ellimc2  21327  limcmpt  21333  limcres  21336  limccnp  21341  limccnp2  21342  limcco  21343  perfdvf  21353  dvreslem  21359  dvcnp2  21369  dvaddbr  21387  dvmulbr  21388  dvcjbr  21398  dvexp  21402  dvrec  21404  dvmptres3  21405  dvmptadd  21409  dvmptmul  21410  dvmptres2  21411  dvmptcmul  21413  dvmptcj  21417  dvmptntr  21420  dvmptco  21421  dvcnvlem  21423  dvef  21427  dvferm1  21432  dvferm2  21434  rolle  21437  dvlipcn  21441  dvle  21454  dvivthlem1  21455  dvivth  21457  lhop1lem  21460  lhop1  21461  lhop2  21462  lhop  21463  dvfsumle  21468  dvfsumge  21469  dvmptrecl  21471  dvfsumrlimf  21472  dvfsumlem2  21474  dvfsumlem3  21475  ftc1lem2  21483  ftc1lem6  21488  itgsubstlem  21495  tdeglem1  21502  tdeglem4  21504  coe1mul3  21546  elply2  21639  plyf  21641  elplyd  21645  plypf1  21655  coeeq2  21685  coemullem  21692  coe1termlem  21700  dvply2g  21726  elqaalem2  21761  taylfvallem  21798  taylf  21801  tayl0  21802  taylpfval  21805  taylpf  21806  taylthlem1  21813  taylthlem2  21814  ulmshftlem  21829  ulmshft  21830  ulmcau  21835  ulmss  21837  ulmdvlem1  21840  ulmdvlem3  21842  mtest  21844  mtestbdd  21845  iblulm  21847  itgulm2  21849  psergf  21852  radcnvlem1  21853  dvradcnv  21861  pserulm  21862  psercn2  21863  pserdvlem2  21868  abelthlem4  21874  abelthlem9  21880  pige3  21954  efif1olem4  21976  logtayl  22080  logccv  22083  loglesqr  22171  leibpi  22312  rlimcnp  22334  rlimcnp2  22335  xrlimcnp  22337  efrlim  22338  dfef2  22339  o1cxp  22343  cxp2lim  22345  amgmlem  22358  basellem2  22394  basellem4  22396  basellem7  22399  basellem9  22401  sqff1o  22495  fsumvma  22527  dchrelbasd  22553  lgsfcl2  22616  lgsqrlem2  22656  lgseisenlem1  22663  lgseisenlem3  22665  lgseisenlem4  22666  chpo1ub  22704  dchrisumlema  22712  dchrmusum2  22718  dchrvmasumiflem1  22725  dchrisum0ff  22731  dchrisum0lem1b  22739  dchrisum0lem2a  22741  logsqvma2  22767  pnt2  22837  pnt  22838  abvcxp  22839  padicabv  22854  axlowdimlem15  23153  nbgraf1olem2  23302  vdgrf  23519  vdgrfif  23520  efghgrp  23811  ipblnfi  24207  ubthlem1  24222  minvecolem1  24226  htthlem  24270  hlimadd  24546  chscllem1  24991  hoaddcl  25113  homulcl  25114  brafn  25302  kbop  25308  cnlnadjlem2  25423  strlem3a  25607  hstrlem3a  25615  off2  25910  xppreima2  25916  fmpt3d  25924  fpwrelmap  25984  gsummptf1o  26198  gsummptun  26199  regsumfsum  26201  gsumvsca1  26202  gsumvsca2  26203  xrge0tsmsd  26204  ordtrestNEW  26303  xrge0mulc1cn  26323  esumf1o  26456  esumadd  26459  esumcst  26466  esumpfinval  26476  esumpcvgval  26479  esumcvg  26487  measinb  26587  measdivcst  26591  mbfmco2  26632  sitgclg  26680  eulerpartlems  26695  dstfrvclim1  26812  gsumncl  26888  gsumnunsn  26889  signstf  26919  lgamgulmlem2  26968  lgamgulmlem6  26972  lgamcvg2  26993  gamcvg  26994  regamcl  26999  relgamcl  27000  erdszelem9  27039  indispcon  27075  cvxpcon  27083  cvmsss2  27115  cvmliftlem6  27131  cvmliftlem8  27133  cvmlift3lem3  27162  divcnvlin  27350  prodfdiv  27362  prodrblem  27393  prodmolem2a  27398  fprodf1o  27410  prodss  27411  fprodss  27412  fprodser  27413  fprodcl2lem  27414  fprodmul  27422  fproddiv  27423  fprodefsum  27436  fprodn0  27441  iprodclim3  27451  iprodefisum  27456  faclimlem2  27501  faclim  27503  faclim2  27505  finixpnum  28367  ptrest  28378  mblfinlem2  28382  volsupnfl  28389  mbfposadd  28392  itg2addnclem2  28397  itg2gt0cn  28400  ibladdnclem  28401  itgaddnclem1  28403  itgaddnc  28405  iblabsnclem  28408  iblabsnc  28409  iblmulc2nc  28410  itgmulc2nclem1  28411  itgmulc2nclem2  28412  itgmulc2nc  28413  itgabsnc  28414  bddiblnc  28415  itggt0cn  28417  ftc1cnnc  28419  ftc1anclem1  28420  ftc1anclem2  28421  ftc1anclem3  28422  ftc1anclem4  28423  ftc1anclem5  28424  ftc1anclem6  28425  ftc1anclem7  28426  ftc1anclem8  28427  ftc1anc  28428  areacirclem4  28440  comppfsc  28532  upixp  28576  totbndbnd  28641  prdsbnd  28645  cntotbnd  28648  rrnequiv  28687  cmpfiiin  28986  mzpclall  29016  mzpindd  29035  fphpdo  29109  dnnumch3  29353  kelac1  29369  dfac21  29372  itgpowd  29543  expgrowth  29562  expcnfg  29726  clim1fr1  29727  itgsinexplem1  29747  wlkiswwlk2lem5  30282  wlknwwlknfun  30295  wlkiswwlkfun  30302  wwlkextfun  30314  clwlkisclwwlklem2a  30400  clwwlkf  30409  clwlkfclwwlk  30470  frgrancvvdeqlem5  30580  numclwlk1lem2f  30638  numclwlk2lem2f  30649  gsumlsscl  30753  pmatcollpw1  30819  lincfsuppcl  30836  linccl  30837  lincvalsc0  30844  lcoc0  30845  linc0scn0  30846  linc1  30848  lincsum  30852  lincscm  30853  lincscmcl  30855  lcoss  30859  lincext1  30877  el0ldep  30889  lincresunit1  30900  lincresunit3  30904  lmod1zr  30924  lsatlss  32481  lflnegcl  32560  lshpkrcl  32601  tendoplcl  34265  tendo0cl  34274  tendoicl  34280
  Copyright terms: Public domain W3C validator