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

Theorem fmptd 5722
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 2660 . 2  |-  ( ph  ->  A. x  e.  A  B  e.  C )
3 fmptd.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43fmpt 5719 . 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 1633    e. wcel 1701   A.wral 2577    e. cmpt 4114   -->wf 5288
This theorem is referenced by:  fmptco  5729  fliftrel  5849  off  6135  caofinvl  6146  curry1f  6254  curry2f  6256  fnwelem  6272  fdiagfn  6854  resixpfo  6897  pw2f1olem  7009  mapxpen  7070  xpmapenlem  7071  unxpdomlem3  7112  wdom2d  7339  cantnfp1lem1  7425  cantnfp1lem2  7426  cantnfp1lem3  7427  cantnflem1d  7435  cantnflem1  7436  cantnf  7440  fseqenlem1  7696  fseqenlem2  7697  dfac8clem  7704  ac5num  7708  acni2  7718  infpwfien  7734  coftr  7944  fin23lem39  8021  isf34lem2  8044  fin1a2lem12  8082  axcc2lem  8107  axdc2lem  8119  axdc3lem4  8124  pwcfsdom  8250  canthp1lem2  8320  wuncval2  8414  gruf  8478  rpnnen1lem1  10389  monoord2  11124  seqf1o  11134  ccatcl  11476  swrdcl  11499  revcl  11526  revlen  11527  ello1mpt  12042  lo1o12  12054  lo1eq  12089  rlimeq  12090  climmpt2  12094  rlimcld2  12099  climrecl  12104  climge0  12105  o1compt  12108  rlimcn1b  12110  rlimcn2  12111  rlimdiv  12166  rlimsqzlem  12169  isercoll2  12189  caurcvg2  12197  caucvg  12198  sumrblem  12231  summolem2a  12235  fsumf1o  12243  sumss  12244  fsumss  12245  fsumcl2lem  12251  fsumadd  12258  isumclim3  12269  isummulc2  12272  fsummulc2  12293  fsumrelem  12312  climfsum  12325  isumshft  12345  divcnv  12359  supcvg  12361  rpnnen2lem2  12541  crt  12893  eulerthlem1  12896  iserodd  12935  prmreclem2  13011  prmreclem6  13015  1arithlem3  13019  4sqlem11  13049  vdwapf  13066  vdwlem2  13076  vdwlem4  13078  vdwlem6  13080  vdwlem10  13084  ramub1lem2  13121  ramcl  13123  prdsplusg  13407  prdsmulr  13408  prdsvsca  13409  mrcflem  13557  mreacs  13609  acsfn  13610  homaf  13911  prfcl  14026  curf1cl  14051  hofcllem  14081  hofcl  14082  yonedalem3a  14097  yonedalem4c  14100  yonedainv  14104  prdspjmhm  14492  pwsco1mhm  14495  pwsco2mhm  14496  gsumz  14507  gsumwspan  14517  vrmdfval  14527  vrmdf  14529  frmdup1  14535  grpinvf  14575  cycsubgcl  14692  cycsubgss  14693  conjghm  14762  conjnmz  14765  divsghm  14768  galactghm  14832  odf1  14924  dfod2  14926  odf1o2  14933  pgpssslw  14974  sylow2blem1  14980  pj1f  15055  frgpmhm  15123  vrgpf  15126  mulgmhm  15176  mulgghm  15177  iscyggen2  15217  cyggenod  15220  iscyg3  15222  gsumzsplit  15255  gsumsplit2  15257  gsumconst  15258  gsummhm2  15261  gsum2d  15272  prdsgsum  15278  dprdfeq0  15306  dprdlub  15310  dprdz  15314  dprd2dlem1  15325  dprd2da  15326  ablfac1b  15354  ablfac2  15373  rnglghm  15437  rngrghm  15438  gsumdixp  15441  abvtrivd  15654  issrngd  15675  lmodvsghm  15735  lspf  15780  asclf  16126  psrass1lem  16172  psrbas  16173  psrmulcllem  16181  psr1cl  16196  psrlidm  16197  psrridm  16198  psrass1  16199  psrdi  16200  psrdir  16201  psrcom  16202  resspsrmul  16210  subrgpsr  16212  mvridlem  16213  mvrf  16218  mplmon  16256  mplmonmul  16257  mplcoe1  16258  mplcoe3  16259  mplcoe2  16260  mplbas2  16261  psrbagsn  16285  evlslem4  16294  evlslem2  16298  psropprmul  16365  coe1mul2  16395  coe1tmmul2  16401  coe1tmmul  16402  ply1coe  16417  gsumfsum  16495  expmhm  16505  expghm  16506  mulgghm2  16515  isphld  16614  pjff  16668  pptbas  16801  tgrest  16946  resttopon  16948  rest0  16956  restfpw  16966  ordtbaslem  16974  ordtuni  16976  ordtrest  16988  cnpfval  17020  pnrmopn  17127  cncmp  17175  discmp  17181  1stcfb  17227  2ndcomap  17240  dis2ndc  17242  lly1stc  17278  kgencmp  17296  ptpjpre1  17322  ptpjcn  17361  ptcldmpt  17364  ptclsg  17365  dfac14  17368  xkoccn  17369  txcnp  17370  ptcnp  17372  txcnmpt  17374  uptx  17375  ptcn  17377  ptrescn  17389  txlm  17398  xkoptsub  17404  xkoco1cn  17407  xkoco2cn  17408  cnmpt11  17413  xkoinjcn  17437  kqffn  17472  pt1hmeo  17553  fbasrn  17631  trfilss  17636  trfg  17638  rnelfmlem  17699  txflf  17753  flfcnp2  17754  fclscmpi  17776  alexsublem  17790  ptcmplem3  17800  symgtgp  17836  subgntr  17841  opnsubg  17842  clsnsg  17844  tgpconcomp  17847  tsmsfbas  17862  eltsms  17867  haustsms  17870  tsmscls  17872  tsms0  17876  tsmsmhm  17880  tgptsmscls  17884  tsmssplit  17886  tsmsxplem1  17887  tsmsxplem2  17888  prdsdsf  17983  prdsxmetlem  17984  imasdsf1olem  17989  prdsbl  18089  stdbdxmet  18113  met1stc  18119  nmf2  18167  nmof  18280  xrge0gsumle  18390  xrge0tsms  18391  metdsf  18404  metdsge  18405  mulc1cncf  18461  cncfmpt2ss  18471  cnmptre  18478  evth  18510  evth2  18511  lebnumlem1  18512  cphnmf  18684  tchcph  18720  cmetcaulem  18767  minveclem1  18841  minveclem3b  18845  ovollb2lem  18900  ovolctb  18902  ovolunlem1a  18908  ovolunlem1  18909  ovoliunlem1  18914  ovoliunlem2  18915  ovoliun  18917  ovolshftlem1  18921  ovolscalem1  18925  ovolicc1  18928  iunmbl  18963  ioombl1lem1  18968  uniioombllem2  18991  uniioombllem3  18993  volsup2  19013  volcn  19014  vitalilem4  19019  vitalilem5  19020  mbfconst  19043  ismbfcn2  19047  mbfeqalem  19050  mbfss  19054  mbfmulc2re  19056  mbfmax  19057  mbfneg  19058  mbfpos  19059  mbfposr  19060  mbfposb  19061  mbfadd  19069  mbfmulc2  19071  mbfsup  19072  mbfinf  19073  mbflimsup  19074  mbflimlem  19075  mbflim  19076  i1f1lem  19097  i1f1  19098  i1fres  19113  itg1climres  19122  mbfi1fseqlem3  19125  mbfi1fseqlem4  19126  mbfi1flimlem  19130  mbfi1flim  19131  mbfmullem2  19132  mbfmul  19134  itg2const2  19149  itg2seq  19150  itg2splitlem  19156  itg2split  19157  itg2monolem1  19158  itg2monolem2  19159  itg2monolem3  19160  itg2mono  19161  itg2i1fseq  19163  itg2i1fseq2  19164  itg2gt0  19168  itg2cnlem1  19169  itg2cnlem2  19170  itg2cn  19171  isibl2  19174  iblss  19212  itgitg1  19216  itgle  19217  itgeqa  19221  itgss3  19222  ibladdlem  19227  itgaddlem1  19230  iblabslem  19235  iblabs  19236  iblabsr  19237  iblmulc2  19238  itgmulc2lem1  19239  bddmulibl  19246  itggt0  19249  itgcn  19250  ellimc2  19280  limcmpt  19286  limcres  19289  limccnp  19294  limccnp2  19295  limcco  19296  perfdvf  19306  dvreslem  19312  dvcnp2  19322  dvaddbr  19340  dvmulbr  19341  dvcjbr  19351  dvexp  19355  dvrec  19357  dvmptres3  19358  dvmptadd  19362  dvmptmul  19363  dvmptres2  19364  dvmptcmul  19366  dvmptcj  19370  dvmptntr  19373  dvmptco  19374  dvcnvlem  19376  dvef  19380  dvferm1  19385  dvferm2  19387  rolle  19390  dvlipcn  19394  dvle  19407  dvivthlem1  19408  dvivth  19410  lhop1lem  19413  lhop1  19414  lhop2  19415  lhop  19416  dvfsumle  19421  dvfsumge  19422  dvmptrecl  19424  dvfsumrlimf  19425  dvfsumlem2  19427  dvfsumlem3  19428  ftc1lem2  19436  ftc1lem6  19441  itgsubstlem  19448  evlslem6  19450  evlslem3  19451  evlslem1  19452  evlsval2  19457  tdeglem1  19497  tdeglem4  19499  coe1mul3  19538  elply2  19631  plyf  19633  elplyd  19637  plypf1  19647  coeeq2  19677  coemullem  19684  coe1termlem  19692  dvply2g  19718  elqaalem2  19753  taylfvallem  19790  taylf  19793  tayl0  19794  taylpfval  19797  taylpf  19798  taylthlem1  19805  taylthlem2  19806  ulmshftlem  19821  ulmshft  19822  ulmcau  19825  ulmss  19827  ulmdvlem1  19830  ulmdvlem3  19832  mtest  19834  iblulm  19836  itgulm2  19838  psergf  19841  radcnvlem1  19842  dvradcnv  19850  pserulm  19851  psercn2  19852  pserdvlem2  19857  abelthlem4  19863  abelthlem9  19869  pige3  19938  efif1olem4  19960  logtayl  20060  logccv  20063  loglesqr  20151  leibpi  20291  rlimcnp  20313  rlimcnp2  20314  xrlimcnp  20316  efrlim  20317  dfef2  20318  o1cxp  20322  cxp2lim  20324  amgmlem  20337  basellem2  20372  basellem4  20374  basellem7  20377  basellem9  20379  sqff1o  20473  fsumvma  20505  dchrelbasd  20531  lgsfcl2  20594  lgsqrlem2  20634  lgseisenlem1  20641  lgseisenlem3  20643  lgseisenlem4  20644  chpo1ub  20682  dchrisumlema  20690  dchrmusum2  20696  dchrvmasumiflem1  20703  dchrisum0ff  20709  dchrisum0lem1b  20717  dchrisum0lem2a  20719  logsqvma2  20745  pnt2  20815  pnt  20816  abvcxp  20817  padicabv  20832  efghgrp  21093  ipblnfi  21489  ubthlem1  21504  minvecolem1  21508  htthlem  21552  hlimadd  21827  chscllem1  22271  hoaddcl  22393  homulcl  22394  brafn  22582  kbop  22588  cnlnadjlem2  22703  strlem3a  22887  hstrlem3a  22895  off2  23204  xrge0tsmsd  23360  esumf1o  23621  esumadd  23624  esumpcvgval  23644  esumcvg  23652  ofcf  23662  measinb  23749  mbfmcst  23783  dstfrvclim1  23909  erdszelem9  24014  indispcon  24049  cvxpcon  24057  cvmsss2  24089  cvmliftlem6  24105  cvmliftlem8  24107  cvmlift3lem3  24136  vdgrf  24175  divcnvlin  24393  prodrblem  24432  prodmolem2a  24437  fprodf1o  24449  prodss  24450  fprodss  24451  fprodser  24452  fprodcl2lem  24453  fprodmul  24461  iprodclim3  24472  faclimlem2  24482  faclim  24484  faclim2  24486  axlowdimlem15  24970  itg2addnclem2  25318  itg2gt0cn  25320  ibladdnclem  25321  itgaddnclem1  25323  itgaddnclem2  25324  itgaddnc  25325  iblabsnclem  25328  iblabsnc  25329  iblmulc2nc  25330  itgmulc2nclem1  25331  itgmulc2nclem2  25332  itgmulc2nc  25333  itgabsnc  25334  bddiblnc  25335  itggt0cn  25337  ftc1cnnc  25339  areacirclem3  25343  areacirclem5  25346  comppfsc  25456  upixp  25552  totbndbnd  25661  prdsbnd  25665  cntotbnd  25668  rrnequiv  25707  cmpfiiin  25920  mzpclall  25953  mzpindd  25972  fphpdo  26048  dnnumch3  26292  kelac1  26309  dfac21  26312  pwssplit0  26335  frlmgsum  26380  uvcff  26388  uvcresum  26390  frlmsplit2  26391  frlmup1  26398  pmtrf  26545  psgnunilem5  26565  mamucl  26604  mamulid  26606  mamurid  26607  mamuass  26608  mamudi  26609  mamudir  26610  mamuvs1  26611  mamuvs2  26612  expgrowth  26700  expcnfg  26874  itgsinexplem1  26896  nbgraf1olem2  27389  vdgref  27565  vdgrefinf  27566  frgrancvvdeqlem5  27626  lsatlss  29004  lflnegcl  29083  lshpkrcl  29124  tendoplcl  30788  tendo0cl  30797  tendoicl  30803
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-mpt 4116  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-fv 5300
  Copyright terms: Public domain W3C validator