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

Theorem fmptd 5646
Description: Domain and co-domain 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 2628 . 2  |-  ( ph  ->  A. x  e.  A  B  e.  C )
3 fmptd.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43fmpt 5643 . 2  |-  ( A. x  e.  A  B  e.  C  <->  F : A --> C )
52, 4sylib 190 1  |-  ( ph  ->  F : A --> C )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    = wceq 1624    e. wcel 1685   A.wral 2545    e. cmpt 4079   -->wf 5218
This theorem is referenced by:  fmptco  5653  fliftrel  5769  off  6055  caofinvl  6066  curry1f  6174  curry2f  6176  fnwelem  6192  fdiagfn  6807  resixpfo  6850  pw2f1olem  6962  mapxpen  7023  xpmapenlem  7024  unxpdomlem3  7065  wdom2d  7290  cantnfp1lem1  7376  cantnfp1lem2  7377  cantnfp1lem3  7378  cantnflem1d  7386  cantnflem1  7387  cantnf  7391  fseqenlem1  7647  fseqenlem2  7648  dfac8clem  7655  ac5num  7659  acni2  7669  infpwfien  7685  coftr  7895  fin23lem39  7972  isf34lem2  7995  fin1a2lem12  8033  axcc2lem  8058  axdc2lem  8070  axdc3lem4  8075  pwcfsdom  8201  canthp1lem2  8271  wuncval2  8365  gruf  8429  rpnnen1lem1  10338  monoord2  11072  seqf1o  11082  ccatcl  11424  swrdcl  11447  revcl  11474  revlen  11475  ello1mpt  11990  lo1o12  12002  lo1eq  12037  rlimeq  12038  climmpt2  12042  rlimcld2  12047  climrecl  12052  climge0  12053  o1compt  12056  rlimcn1b  12058  rlimcn2  12059  rlimdiv  12114  rlimsqzlem  12117  isercoll2  12137  caurcvg2  12145  caucvg  12146  sumrblem  12179  summolem2a  12183  fsumf1o  12191  sumss  12192  fsumss  12193  fsumcl2lem  12199  fsumadd  12206  isumclim3  12217  isummulc2  12220  fsummulc2  12241  fsumrelem  12260  climfsum  12273  isumshft  12293  divcnv  12307  supcvg  12309  rpnnen2lem2  12489  crt  12841  eulerthlem1  12844  iserodd  12883  prmreclem2  12959  prmreclem6  12963  1arithlem3  12967  4sqlem11  12997  vdwapf  13014  vdwlem2  13024  vdwlem4  13026  vdwlem6  13028  vdwlem10  13032  ramub1lem2  13069  ramcl  13071  prdsplusg  13353  prdsmulr  13354  prdsvsca  13355  mrcflem  13503  mreacs  13555  acsfn  13556  homaf  13857  prfcl  13972  curf1cl  13997  hofcllem  14027  hofcl  14028  yonedalem3a  14043  yonedalem4c  14046  yonedainv  14050  prdspjmhm  14438  pwsco1mhm  14441  pwsco2mhm  14442  gsumz  14453  gsumwspan  14463  vrmdfval  14473  vrmdf  14475  frmdup1  14481  grpinvf  14521  cycsubgcl  14638  cycsubgss  14639  conjghm  14708  conjnmz  14711  divsghm  14714  galactghm  14778  odf1  14870  dfod2  14872  odf1o2  14879  pgpssslw  14920  sylow2blem1  14926  pj1f  15001  frgpmhm  15069  vrgpf  15072  mulgmhm  15122  mulgghm  15123  iscyggen2  15163  cyggenod  15166  iscyg3  15168  gsumzsplit  15201  gsumsplit2  15203  gsumconst  15204  gsummhm2  15207  gsum2d  15218  prdsgsum  15224  dprdfeq0  15252  dprdlub  15256  dprdz  15260  dprd2dlem1  15271  dprd2da  15272  ablfac1b  15300  ablfac2  15319  rnglghm  15383  rngrghm  15384  gsumdixp  15387  abvtrivd  15600  issrngd  15621  lmodvsghm  15681  lspf  15726  asclf  16072  psrass1lem  16118  psrbas  16119  psrmulcllem  16127  psr1cl  16142  psrlidm  16143  psrridm  16144  psrass1  16145  psrdi  16146  psrdir  16147  psrcom  16148  resspsrmul  16156  subrgpsr  16158  mvridlem  16159  mvrf  16164  mplmon  16202  mplmonmul  16203  mplcoe1  16204  mplcoe3  16205  mplcoe2  16206  mplbas2  16207  psrbagsn  16231  evlslem4  16240  evlslem2  16244  psropprmul  16311  coe1mul2  16341  coe1tmmul2  16347  coe1tmmul  16348  ply1coe  16363  gsumfsum  16434  expmhm  16444  expghm  16445  mulgghm2  16454  isphld  16553  pjff  16607  pptbas  16740  tgrest  16885  resttopon  16887  rest0  16895  restfpw  16905  ordtbaslem  16913  ordtuni  16915  ordtrest  16927  cnpfval  16959  pnrmopn  17066  cncmp  17114  discmp  17120  1stcfb  17166  2ndcomap  17179  dis2ndc  17181  lly1stc  17217  kgencmp  17235  ptpjpre1  17261  ptpjcn  17300  ptcldmpt  17303  ptclsg  17304  dfac14  17307  xkoccn  17308  txcnp  17309  ptcnp  17311  txcnmpt  17313  uptx  17314  ptcn  17316  ptrescn  17328  txlm  17337  xkoptsub  17343  xkoco1cn  17346  xkoco2cn  17347  cnmpt11  17352  xkoinjcn  17376  kqffn  17411  pt1hmeo  17492  fbasrn  17574  trfilss  17579  trfg  17581  rnelfmlem  17642  txflf  17696  flfcnp2  17697  fclscmpi  17719  alexsublem  17733  ptcmplem3  17743  symgtgp  17779  subgntr  17784  opnsubg  17785  clsnsg  17787  tgpconcomp  17790  tsmsfbas  17805  eltsms  17810  haustsms  17813  tsmscls  17815  tsms0  17819  tsmsmhm  17823  tgptsmscls  17827  tsmssplit  17829  tsmsxplem1  17830  tsmsxplem2  17831  prdsdsf  17926  prdsxmetlem  17927  imasdsf1olem  17932  prdsbl  18032  stdbdxmet  18056  met1stc  18062  nmf2  18110  nmof  18223  xrge0gsumle  18333  xrge0tsms  18334  metdsf  18347  metdsge  18348  mulc1cncf  18404  cncfmpt2ss  18414  cnmptre  18420  evth  18452  evth2  18453  lebnumlem1  18454  cphnmf  18626  tchcph  18662  cmetcaulem  18709  minveclem1  18783  minveclem3b  18787  ovollb2lem  18842  ovolctb  18844  ovolunlem1a  18850  ovolunlem1  18851  ovoliunlem1  18856  ovoliunlem2  18857  ovoliun  18859  ovolshftlem1  18863  ovolscalem1  18867  ovolicc1  18870  iunmbl  18905  ioombl1lem1  18910  uniioombllem2  18933  uniioombllem3  18935  volsup2  18955  volcn  18956  vitalilem4  18961  vitalilem5  18962  mbfconst  18985  ismbfcn2  18989  mbfeqalem  18992  mbfss  18996  mbfmulc2re  18998  mbfmax  18999  mbfneg  19000  mbfpos  19001  mbfposr  19002  mbfposb  19003  mbfadd  19011  mbfmulc2  19013  mbfsup  19014  mbfinf  19015  mbflimsup  19016  mbflimlem  19017  mbflim  19018  i1f1lem  19039  i1f1  19040  i1fres  19055  itg1climres  19064  mbfi1fseqlem3  19067  mbfi1fseqlem4  19068  mbfi1flimlem  19072  mbfi1flim  19073  mbfmullem2  19074  mbfmul  19076  itg2const2  19091  itg2seq  19092  itg2splitlem  19098  itg2split  19099  itg2monolem1  19100  itg2monolem2  19101  itg2monolem3  19102  itg2mono  19103  itg2i1fseq  19105  itg2i1fseq2  19106  itg2gt0  19110  itg2cnlem1  19111  itg2cnlem2  19112  itg2cn  19113  isibl2  19116  iblss  19154  itgitg1  19158  itgle  19159  itgeqa  19163  itgss3  19164  ibladdlem  19169  itgaddlem1  19172  iblabslem  19177  iblabs  19178  iblabsr  19179  iblmulc2  19180  itgmulc2lem1  19181  bddmulibl  19188  itggt0  19191  itgcn  19192  ellimc2  19222  limcmpt  19228  limcres  19231  limccnp  19236  limccnp2  19237  limcco  19238  perfdvf  19248  dvreslem  19254  dvcnp2  19264  dvaddbr  19282  dvmulbr  19283  dvcjbr  19293  dvexp  19297  dvrec  19299  dvmptres3  19300  dvmptadd  19304  dvmptmul  19305  dvmptres2  19306  dvmptcmul  19308  dvmptcj  19312  dvmptntr  19315  dvmptco  19316  dvcnvlem  19318  dvef  19322  dvferm1  19327  dvferm2  19329  rolle  19332  dvlipcn  19336  dvle  19349  dvivthlem1  19350  dvivth  19352  lhop1lem  19355  lhop1  19356  lhop2  19357  lhop  19358  dvfsumle  19363  dvfsumge  19364  dvmptrecl  19366  dvfsumrlimf  19367  dvfsumlem2  19369  dvfsumlem3  19370  ftc1lem2  19378  ftc1lem6  19383  itgsubstlem  19390  evlslem6  19392  evlslem3  19393  evlslem1  19394  evlsval2  19399  tdeglem1  19439  tdeglem4  19441  coe1mul3  19480  elply2  19573  plyf  19575  elplyd  19579  plypf1  19589  coeeq2  19619  coemullem  19626  coe1termlem  19634  dvply2g  19660  elqaalem2  19695  taylfvallem  19732  taylf  19735  tayl0  19736  taylpfval  19739  taylpf  19740  taylthlem1  19747  taylthlem2  19748  ulmshftlem  19763  ulmshft  19764  ulmcau  19767  ulmss  19769  ulmdvlem1  19772  ulmdvlem3  19774  mtest  19776  iblulm  19778  itgulm2  19780  psergf  19783  radcnvlem1  19784  dvradcnv  19792  pserulm  19793  psercn2  19794  pserdvlem2  19799  abelthlem4  19805  abelthlem9  19811  pige3  19880  efif1olem4  19902  logtayl  20002  logccv  20005  loglesqr  20093  leibpi  20233  rlimcnp  20255  rlimcnp2  20256  xrlimcnp  20258  efrlim  20259  dfef2  20260  o1cxp  20264  cxp2lim  20266  amgmlem  20279  basellem2  20314  basellem4  20316  basellem7  20319  basellem9  20321  sqff1o  20415  fsumvma  20447  dchrelbasd  20473  lgsfcl2  20536  lgsqrlem2  20576  lgseisenlem1  20583  lgseisenlem3  20585  lgseisenlem4  20586  chpo1ub  20624  dchrisumlema  20632  dchrmusum2  20638  dchrvmasumiflem1  20645  dchrisum0ff  20651  dchrisum0lem1b  20659  dchrisum0lem2a  20661  logsqvma2  20687  pnt2  20757  pnt  20758  abvcxp  20759  padicabv  20774  efghgrp  21033  ipblnfi  21427  ubthlem1  21442  minvecolem1  21446  htthlem  21490  hlimadd  21765  chscllem1  22209  hoaddcl  22331  homulcl  22332  brafn  22520  kbop  22526  cnlnadjlem2  22641  strlem3a  22825  hstrlem3a  22833  erdszelem9  23135  indispcon  23170  cvxpcon  23178  cvmsss2  23210  cvmliftlem6  23226  cvmliftlem8  23228  cvmlift3lem3  23257  vdgrf  23296  axlowdimlem15  23992  prmapcp2  24557  prjmapcp  24565  claddrv  25047  zernpl  25053  addassv  25056  cnegvex2  25060  rnegvex2  25061  domcatfun  25325  codcatfun  25334  idcatfun  25341  clscnc  25410  comppfsc  25707  upixp  25803  totbndbnd  25913  prdsbnd  25917  cntotbnd  25920  rrnequiv  25959  cmpfiiin  26172  mzpclall  26205  mzpindd  26224  fphpdo  26300  dnnumch3  26544  kelac1  26561  dfac21  26564  pwssplit0  26587  frlmgsum  26632  uvcff  26640  uvcresum  26642  frlmsplit2  26643  frlmup1  26650  pmtrf  26797  psgnunilem5  26817  mamucl  26856  mamulid  26858  mamurid  26859  mamuass  26860  mamudi  26861  mamudir  26862  mamuvs1  26863  mamuvs2  26864  expgrowth  26952  expcnfg  27126  itgsinexplem1  27148  lsatlss  28454  lflnegcl  28533  lshpkrcl  28574  tendoplcl  30238  tendo0cl  30247  tendoicl  30253
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-mpt 4081  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-fun 5224  df-fn 5225  df-f 5226  df-fv 5230
  Copyright terms: Public domain W3C validator