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

Theorem fmptd 5852
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 2749 . 2  |-  ( ph  ->  A. x  e.  A  B  e.  C )
3 fmptd.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43fmpt 5849 . 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 1649    e. wcel 1721   A.wral 2666    e. cmpt 4226   -->wf 5409
This theorem is referenced by:  fmptco  5860  fliftrel  5989  off  6279  caofinvl  6290  curry1f  6399  curry2f  6401  fnwelem  6420  fdiagfn  7016  resixpfo  7059  pw2f1olem  7171  mapxpen  7232  xpmapenlem  7233  unxpdomlem3  7274  wdom2d  7504  cantnfp1lem1  7590  cantnfp1lem2  7591  cantnfp1lem3  7592  cantnflem1d  7600  cantnflem1  7601  cantnf  7605  fseqenlem1  7861  fseqenlem2  7862  dfac8clem  7869  ac5num  7873  acni2  7883  infpwfien  7899  coftr  8109  fin23lem39  8186  isf34lem2  8209  fin1a2lem12  8247  axcc2lem  8272  axdc2lem  8284  axdc3lem4  8289  pwcfsdom  8414  canthp1lem2  8484  wuncval2  8578  gruf  8642  rpnnen1lem1  10556  monoord2  11309  seqf1o  11319  ccatcl  11698  swrdcl  11721  revcl  11748  revlen  11749  ello1mpt  12270  lo1o12  12282  lo1eq  12317  rlimeq  12318  climmpt2  12322  rlimcld2  12327  climrecl  12332  climge0  12333  o1compt  12336  rlimcn1b  12338  rlimcn2  12339  rlimdiv  12394  rlimsqzlem  12397  isercoll2  12417  caurcvg2  12426  caucvg  12427  sumrblem  12460  summolem2a  12464  fsumf1o  12472  sumss  12473  fsumss  12474  fsumcl2lem  12480  fsumadd  12487  isumclim3  12498  isummulc2  12501  fsummulc2  12522  fsumrelem  12541  climfsum  12554  isumshft  12574  divcnv  12588  supcvg  12590  rpnnen2lem2  12770  crt  13122  eulerthlem1  13125  iserodd  13164  prmreclem2  13240  prmreclem6  13244  1arithlem3  13248  4sqlem11  13278  vdwapf  13295  vdwlem2  13305  vdwlem4  13307  vdwlem6  13309  vdwlem10  13313  ramub1lem2  13350  ramcl  13352  prdsplusg  13636  prdsmulr  13637  prdsvsca  13638  mrcflem  13786  mreacs  13838  acsfn  13839  homaf  14140  prfcl  14255  curf1cl  14280  hofcllem  14310  hofcl  14311  yonedalem3a  14326  yonedalem4c  14329  yonedainv  14333  prdspjmhm  14721  pwsco1mhm  14724  pwsco2mhm  14725  gsumz  14736  gsumwspan  14746  vrmdfval  14756  vrmdf  14758  frmdup1  14764  grpinvf  14804  cycsubgcl  14921  cycsubgss  14922  conjghm  14991  conjnmz  14994  divsghm  14997  galactghm  15061  odf1  15153  dfod2  15155  odf1o2  15162  pgpssslw  15203  sylow2blem1  15209  pj1f  15284  frgpmhm  15352  vrgpf  15355  mulgmhm  15405  mulgghm  15406  iscyggen2  15446  cyggenod  15449  iscyg3  15451  gsumzsplit  15484  gsumsplit2  15486  gsumconst  15487  gsummhm2  15490  gsum2d  15501  prdsgsum  15507  dprdfeq0  15535  dprdlub  15539  dprdz  15543  dprd2dlem1  15554  dprd2da  15555  ablfac1b  15583  ablfac2  15602  rnglghm  15666  rngrghm  15667  gsumdixp  15670  abvtrivd  15883  issrngd  15904  lmodvsghm  15960  lspf  16005  asclf  16351  psrass1lem  16397  psrbas  16398  psrmulcllem  16406  psr1cl  16421  psrlidm  16422  psrridm  16423  psrass1  16424  psrdi  16425  psrdir  16426  psrcom  16427  resspsrmul  16435  subrgpsr  16437  mvridlem  16438  mvrf  16443  mplmon  16481  mplmonmul  16482  mplcoe1  16483  mplcoe3  16484  mplcoe2  16485  mplbas2  16486  psrbagsn  16510  evlslem4  16519  evlslem2  16523  psropprmul  16587  coe1mul2  16617  coe1tmmul2  16623  coe1tmmul  16624  ply1coe  16639  gsumfsum  16721  expmhm  16731  expghm  16732  mulgghm2  16741  isphld  16840  pjff  16894  pptbas  17027  tgrest  17177  resttopon  17179  rest0  17187  restfpw  17197  ordtbaslem  17206  ordtuni  17208  ordtrest  17220  cnpfval  17252  pnrmopn  17361  cncmp  17409  discmp  17415  1stcfb  17461  2ndcomap  17474  dis2ndc  17476  lly1stc  17512  kgencmp  17530  ptpjpre1  17556  ptpjcn  17596  ptcldmpt  17599  ptclsg  17600  dfac14  17603  xkoccn  17604  txcnp  17605  ptcnp  17607  txcnmpt  17609  uptx  17610  ptcn  17612  ptrescn  17624  txlm  17633  xkoptsub  17639  xkoco1cn  17642  xkoco2cn  17643  cnmpt11  17648  xkoinjcn  17672  kqffn  17710  pt1hmeo  17791  fbasrn  17869  trfilss  17874  trfg  17876  rnelfmlem  17937  txflf  17991  flfcnp2  17992  fclscmpi  18014  alexsublem  18028  ptcmplem3  18038  symgtgp  18084  subgntr  18089  opnsubg  18090  clsnsg  18092  tgpconcomp  18095  tsmsfbas  18110  eltsms  18115  haustsms  18118  tsmscls  18120  tsms0  18124  tsmsmhm  18128  tgptsmscls  18132  tsmssplit  18134  tsmsxplem1  18135  tsmsxplem2  18136  ustuqtop0  18223  prdsdsf  18350  prdsxmetlem  18351  imasdsf1olem  18356  prdsbl  18474  stdbdxmet  18498  met1stc  18504  nmf2  18593  nmof  18706  xrge0gsumle  18817  xrge0tsms  18818  metdsf  18831  metdsge  18832  mulc1cncf  18888  cncfmpt2ss  18898  cnmptre  18905  evth  18937  evth2  18938  lebnumlem1  18939  cphnmf  19111  tchcph  19147  cmetcaulem  19194  minveclem1  19278  minveclem3b  19282  ovollb2lem  19337  ovolctb  19339  ovolunlem1a  19345  ovolunlem1  19346  ovoliunlem1  19351  ovoliunlem2  19352  ovoliun  19354  ovolshftlem1  19358  ovolscalem1  19362  ovolicc1  19365  iunmbl  19400  ioombl1lem1  19405  uniioombllem2  19428  uniioombllem3  19430  volsup2  19450  volcn  19451  vitalilem4  19456  vitalilem5  19457  mbfconst  19480  ismbfcn2  19484  mbfeqalem  19487  mbfss  19491  mbfmulc2re  19493  mbfmax  19494  mbfneg  19495  mbfpos  19496  mbfposr  19497  mbfposb  19498  mbfadd  19506  mbfmulc2  19508  mbfsup  19509  mbfinf  19510  mbflimsup  19511  mbflimlem  19512  mbflim  19513  i1f1lem  19534  i1f1  19535  i1fres  19550  itg1climres  19559  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  mbfi1flimlem  19567  mbfi1flim  19568  mbfmullem2  19569  mbfmul  19571  itg2const2  19586  itg2seq  19587  itg2splitlem  19593  itg2split  19594  itg2monolem1  19595  itg2monolem2  19596  itg2monolem3  19597  itg2mono  19598  itg2i1fseq  19600  itg2i1fseq2  19601  itg2gt0  19605  itg2cnlem1  19606  itg2cnlem2  19607  itg2cn  19608  isibl2  19611  iblss  19649  itgitg1  19653  itgle  19654  itgeqa  19658  itgss3  19659  ibladdlem  19664  itgaddlem1  19667  iblabslem  19672  iblabs  19673  iblabsr  19674  iblmulc2  19675  itgmulc2lem1  19676  bddmulibl  19683  itggt0  19686  itgcn  19687  ellimc2  19717  limcmpt  19723  limcres  19726  limccnp  19731  limccnp2  19732  limcco  19733  perfdvf  19743  dvreslem  19749  dvcnp2  19759  dvaddbr  19777  dvmulbr  19778  dvcjbr  19788  dvexp  19792  dvrec  19794  dvmptres3  19795  dvmptadd  19799  dvmptmul  19800  dvmptres2  19801  dvmptcmul  19803  dvmptcj  19807  dvmptntr  19810  dvmptco  19811  dvcnvlem  19813  dvef  19817  dvferm1  19822  dvferm2  19824  rolle  19827  dvlipcn  19831  dvle  19844  dvivthlem1  19845  dvivth  19847  lhop1lem  19850  lhop1  19851  lhop2  19852  lhop  19853  dvfsumle  19858  dvfsumge  19859  dvmptrecl  19861  dvfsumrlimf  19862  dvfsumlem2  19864  dvfsumlem3  19865  ftc1lem2  19873  ftc1lem6  19878  itgsubstlem  19885  evlslem6  19887  evlslem3  19888  evlslem1  19889  evlsval2  19894  tdeglem1  19934  tdeglem4  19936  coe1mul3  19975  elply2  20068  plyf  20070  elplyd  20074  plypf1  20084  coeeq2  20114  coemullem  20121  coe1termlem  20129  dvply2g  20155  elqaalem2  20190  taylfvallem  20227  taylf  20230  tayl0  20231  taylpfval  20234  taylpf  20235  taylthlem1  20242  taylthlem2  20243  ulmshftlem  20258  ulmshft  20259  ulmcau  20264  ulmss  20266  ulmdvlem1  20269  ulmdvlem3  20271  mtest  20273  mtestbdd  20274  iblulm  20276  itgulm2  20278  psergf  20281  radcnvlem1  20282  dvradcnv  20290  pserulm  20291  psercn2  20292  pserdvlem2  20297  abelthlem4  20303  abelthlem9  20309  pige3  20378  efif1olem4  20400  logtayl  20504  logccv  20507  loglesqr  20595  leibpi  20735  rlimcnp  20757  rlimcnp2  20758  xrlimcnp  20760  efrlim  20761  dfef2  20762  o1cxp  20766  cxp2lim  20768  amgmlem  20781  basellem2  20817  basellem4  20819  basellem7  20822  basellem9  20824  sqff1o  20918  fsumvma  20950  dchrelbasd  20976  lgsfcl2  21039  lgsqrlem2  21079  lgseisenlem1  21086  lgseisenlem3  21088  lgseisenlem4  21089  chpo1ub  21127  dchrisumlema  21135  dchrmusum2  21141  dchrvmasumiflem1  21148  dchrisum0ff  21154  dchrisum0lem1b  21162  dchrisum0lem2a  21164  logsqvma2  21190  pnt2  21260  pnt  21261  abvcxp  21262  padicabv  21277  nbgraf1olem2  21405  vdgrf  21622  vdgrfif  21623  efghgrp  21914  ipblnfi  22310  ubthlem1  22325  minvecolem1  22329  htthlem  22373  hlimadd  22648  chscllem1  23092  hoaddcl  23214  homulcl  23215  brafn  23403  kbop  23409  cnlnadjlem2  23524  strlem3a  23708  hstrlem3a  23716  off2  24007  xppreima2  24013  fmpt3d  24023  xrge0tsmsd  24176  xrge0mulc1cn  24280  esumf1o  24398  esumadd  24401  esumcst  24408  esumpfinval  24418  esumpcvgval  24421  esumcvg  24429  measinb  24528  measdivcst  24532  mbfmco2  24568  sitgclg  24609  dstfrvclim1  24688  lgamgulmlem2  24767  lgamgulmlem6  24771  lgamcvg2  24792  gamcvg  24793  regamcl  24798  relgamcl  24799  erdszelem9  24838  indispcon  24874  cvxpcon  24882  cvmsss2  24914  cvmliftlem6  24930  cvmliftlem8  24932  cvmlift3lem3  24961  divcnvlin  25165  prodfdiv  25177  prodrblem  25208  prodmolem2a  25213  fprodf1o  25225  prodss  25226  fprodss  25227  fprodser  25228  fprodcl2lem  25229  fprodmul  25237  fproddiv  25238  fprodefsum  25251  fprodn0  25256  iprodclim3  25266  iprodefisum  25271  faclimlem2  25311  faclim  25313  faclim2  25315  axlowdimlem15  25799  mblfinlem  26143  volsupnfl  26150  mbfposadd  26153  itg2addnclem2  26156  itg2gt0cn  26159  ibladdnclem  26160  itgaddnclem1  26162  itgaddnc  26164  iblabsnclem  26167  iblabsnc  26168  iblmulc2nc  26169  itgmulc2nclem1  26170  itgmulc2nclem2  26171  itgmulc2nc  26172  itgabsnc  26173  bddiblnc  26174  itggt0cn  26176  ftc1cnnc  26178  areacirclem3  26182  areacirclem5  26185  comppfsc  26277  upixp  26321  totbndbnd  26388  prdsbnd  26392  cntotbnd  26395  rrnequiv  26434  cmpfiiin  26641  mzpclall  26674  mzpindd  26693  fphpdo  26768  dnnumch3  27012  kelac1  27029  dfac21  27032  pwssplit0  27055  frlmgsum  27100  uvcff  27108  uvcresum  27110  frlmsplit2  27111  frlmup1  27118  pmtrf  27265  psgnunilem5  27285  mamucl  27324  mamulid  27326  mamurid  27327  mamuass  27328  mamudi  27329  mamudir  27330  mamuvs1  27331  mamuvs2  27332  expgrowth  27420  expcnfg  27593  clim1fr1  27594  itgsinexplem1  27615  frgrancvvdeqlem5  28137  lsatlss  29479  lflnegcl  29558  lshpkrcl  29599  tendoplcl  31263  tendo0cl  31272  tendoicl  31278
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421
  Copyright terms: Public domain W3C validator