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

Theorem fmptd 6276
Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.)
Hypotheses
Ref Expression
fmptd.1 ((𝜑𝑥𝐴) → 𝐵𝐶)
fmptd.2 𝐹 = (𝑥𝐴𝐵)
Assertion
Ref Expression
fmptd (𝜑𝐹:𝐴𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜑,𝑥
Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem fmptd
StepHypRef Expression
1 fmptd.1 . . 3 ((𝜑𝑥𝐴) → 𝐵𝐶)
21ralrimiva 2948 . 2 (𝜑 → ∀𝑥𝐴 𝐵𝐶)
3 fmptd.2 . . 3 𝐹 = (𝑥𝐴𝐵)
43fmpt 6273 . 2 (∀𝑥𝐴 𝐵𝐶𝐹:𝐴𝐶)
52, 4sylib 206 1 (𝜑𝐹:𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  wral 2895  cmpt 4637  wf 5785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pr 4827
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4942  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-fv 5797
This theorem is referenced by:  fmpt3d  6277  fliftrel  6435  off  6787  caofinvl  6799  curry1f  7135  curry2f  7137  fnwelem  7156  fdiagfn  7764  resixpfo  7809  pw2f1olem  7926  mapxpen  7988  xpmapenlem  7989  unxpdomlem3  8028  fsuppmptdm  8146  fsuppmptif  8165  wdom2d  8345  cantnfp1lem1  8435  cantnfp1lem2  8436  cantnfp1lem3  8437  cantnflem1d  8445  cantnflem1  8446  cantnf  8450  fseqenlem1  8707  fseqenlem2  8708  dfac8clem  8715  ac5num  8719  acni2  8729  infpwfien  8745  coftr  8955  fin23lem39  9032  isf34lem2  9055  fin1a2lem12  9093  axcc2lem  9118  axdc2lem  9130  axdc3lem4  9135  pwcfsdom  9261  canthp1lem2  9331  wuncval2  9425  gruf  9489  rpnnen1lem1  11649  rpnnen1lem1OLD  11655  monoord2  12651  seqf1o  12661  ccatcl  13160  swrdcl  13219  revcl  13309  revlen  13310  ello1mpt  14048  lo1o12  14060  lo1eq  14095  rlimeq  14096  climmpt2  14100  climrecl  14110  climge0  14111  o1compt  14114  rlimcn1b  14116  rlimdiv  14172  isercoll2  14195  caurcvg2  14204  caucvg  14205  sumrblem  14237  summolem2a  14241  fsumf1o  14249  sumss  14250  fsumss  14251  fsumcl2lem  14257  fsumadd  14265  isumclim3  14280  isummulc2  14283  fsummulc2  14306  fsumrelem  14328  climfsum  14341  isumshft  14358  divcnv  14372  supcvg  14375  prodfdiv  14415  prodrblem  14446  prodmolem2a  14451  fprodf1o  14463  prodss  14464  fprodss  14465  fprodser  14466  fprodcl2lem  14467  fprodmul  14477  fproddiv  14478  fprodn0  14496  iprodclim3  14518  fprodefsum  14612  rpnnen2lem2  14731  crth  15269  eulerthlem1  15272  iserodd  15326  prmreclem2  15407  prmreclem6  15411  1arithlem3  15415  4sqlem11  15445  vdwapf  15462  vdwlem2  15472  vdwlem4  15474  vdwlem6  15476  vdwlem10  15480  ramub1lem2  15517  ramcl  15519  prmodvdslcmf  15537  prmgaplcm  15550  prdsplusg  15889  prdsmulr  15890  prdsvsca  15891  mrcflem  16037  mreacs  16090  acsfn  16091  homaf  16451  funcestrcsetclem3  16553  funcsetcestrclem3  16567  prfcl  16614  curf1cl  16639  hofcllem  16669  hofcl  16670  yonedalem3a  16685  yonedalem4c  16688  yonedainv  16692  prdspjmhm  17138  pwsco1mhm  17141  pwsco2mhm  17142  gsumz  17145  gsumwspan  17154  vrmdfval  17164  vrmdf  17166  frmdup1  17172  grpinvf  17237  cycsubgcl  17391  cycsubgss  17392  conjghm  17462  conjnmz  17465  qusghm  17468  galactghm  17594  symgextf  17608  symgfixf  17627  pmtrf  17646  pmtrdifwrdellem1  17672  psgnunilem5  17685  odf1  17750  dfod2  17752  odf1o2  17759  pgpssslw  17800  sylow2blem1  17806  pj1f  17881  frgpmhm  17949  vrgpf  17952  mulgmhm  18004  mulgghm  18005  iscyggen2  18054  cyggenod  18057  iscyg3  18059  gsummptfsadd  18095  gsumzsplit  18098  gsumsplit2  18100  gsummptfidmsplitres  18102  gsumconst  18105  gsummptshft  18107  gsummhm2  18110  gsummptmhm  18111  gsummptfidminv  18118  gsummptfssub  18120  gsumzunsnd  18126  gsummptf1o  18133  gsummpt1n0  18135  gsum2dlem1  18140  gsum2dlem2  18141  gsum2d  18142  prdsgsum  18148  dprdfeq0  18192  dprdlub  18196  dprdz  18200  dprd2dlem1  18211  dprd2da  18212  ablfac1b  18240  ablfac2  18259  srglmhm  18306  srgrmhm  18307  ringlghm  18375  ringrghm  18376  gsumdixp  18380  abvtrivd  18611  issrngd  18632  lmodvsghm  18695  lspf  18743  pwssplit0  18827  asclf  19106  snifpsrbag  19135  psrass1lem  19146  psrmulcllem  19156  psr1cl  19171  psrlidm  19172  psrridm  19173  psrcom  19178  resspsrmul  19186  subrgpsr  19188  mvrf  19193  mplmon  19232  mplmonmul  19233  mplcoe1  19234  mplcoe5lem  19236  mplcoe5  19237  mplbas2  19239  psrbagsn  19264  evlslem4  19277  evlslem2  19281  evlslem6  19282  evlslem3  19283  evlslem1  19284  evlsval2  19289  psropprmul  19377  coe1mul2  19408  coe1tmmul2  19415  coe1tmmul  19416  ply1coe  19435  gsumsmonply1  19442  gsummoncoe1  19443  gsumfsum  19580  regsumfsum  19581  expmhm  19582  expghm  19610  mulgghm2  19611  evpmodpmf1o  19708  isphld  19765  pjff  19822  frlmgsum  19877  frlmsplit2  19878  frlmphl  19886  uvcff  19896  uvcresum  19898  frlmup1  19903  mamulid  20013  mamurid  20014  scmatf  20101  mdetf  20167  mdetunilem9  20192  mdetuni0  20193  mdetmul  20195  maduf  20213  smadiadetlem3lem1  20238  cpm2mf  20323  m2cpmfo  20327  pmatcollpw1  20347  pmatcollpw3lem  20354  pmatcollpw3fi1lem1  20357  pmatcollpw3fi1lem2  20358  pm2mpcl  20368  mply1topmatcl  20376  mp2pm2mplem2  20378  mp2pm2mp  20382  pm2mpmhmlem2  20390  chfacfisf  20425  chfacfisfcpmat  20426  cpmidpmatlem2  20442  cayhamlem4  20459  pptbas  20569  tgrest  20720  resttopon  20722  rest0  20730  restfpw  20740  ordtbaslem  20749  ordtuni  20751  ordtrest  20763  cnpfval  20795  pnrmopn  20904  cncmp  20952  discmp  20958  1stcfb  21005  2ndcomap  21018  dis2ndc  21020  lly1stc  21056  comppfsc  21092  kgencmp  21105  ptpjpre1  21131  ptpjcn  21171  ptcldmpt  21174  ptclsg  21175  dfac14  21178  xkoccn  21179  txcnp  21180  ptcnp  21182  txcnmpt  21184  uptx  21185  ptcn  21187  ptrescn  21199  txlm  21208  xkoptsub  21214  xkoco1cn  21217  xkoco2cn  21218  cnmpt11  21223  xkoinjcn  21247  kqffn  21285  pt1hmeo  21366  fbasrn  21445  trfilss  21450  trfg  21452  rnelfmlem  21513  txflf  21567  flfcnp2  21568  fclscmpi  21590  alexsublem  21605  ptcmplem3  21615  symgtgp  21662  subgntr  21667  opnsubg  21668  clsnsg  21670  tgpconcomp  21673  tsmsfbas  21688  eltsms  21693  haustsms  21696  tsmscls  21698  tsms0  21702  tsmsmhm  21706  tgptsmscls  21710  tsmssplit  21712  tsmsxplem1  21713  tsmsxplem2  21714  ustuqtop0  21801  prdsdsf  21929  prdsxmetlem  21930  imasdsf1olem  21935  prdsbl  22053  stdbdxmet  22077  met1stc  22083  nmf2  22154  xrge0gsumle  22391  xrge0tsms  22392  metdsf  22406  metdsge  22407  mulc1cncf  22463  cncfmpt2ss  22473  cnmptre  22481  evth  22513  evth2  22514  lebnumlem1  22515  cphnmf  22747  tchcph  22788  cmetcaulem  22838  rrxmval  22940  minveclem1  22947  minveclem3b  22951  ovollb2lem  23007  ovolctb  23009  ovolunlem1a  23015  ovolunlem1  23016  ovoliunlem1  23021  ovoliunlem2  23022  ovoliun  23024  ovolshftlem1  23028  ovolscalem1  23032  ovolicc1  23035  iunmbl  23072  ioombl1lem1  23077  uniioombllem2  23101  uniioombllem3  23103  volsup2  23123  volcn  23124  vitalilem4  23130  vitalilem5  23131  mbfconst  23152  ismbfcn2  23156  mbfeqalem  23159  mbfss  23163  mbfmulc2re  23165  mbfmax  23166  mbfneg  23167  mbfpos  23168  mbfposr  23169  mbfposb  23170  mbfadd  23178  mbfmulc2  23180  mbfsup  23181  mbfinf  23182  mbflimsup  23183  mbflimlem  23184  mbflim  23185  i1f1lem  23206  i1f1  23207  i1fres  23222  itg1climres  23231  mbfi1fseqlem3  23234  mbfi1fseqlem4  23235  mbfi1flimlem  23239  mbfi1flim  23240  mbfmullem2  23241  mbfmul  23243  itg2const2  23258  itg2seq  23259  itg2splitlem  23265  itg2split  23266  itg2monolem1  23267  itg2monolem2  23268  itg2monolem3  23269  itg2mono  23270  itg2i1fseq  23272  itg2i1fseq2  23273  itg2gt0  23277  itg2cnlem1  23278  itg2cnlem2  23279  itg2cn  23280  iblss  23321  itgitg1  23325  itgle  23326  itgeqa  23330  itgss3  23331  ibladdlem  23336  itgaddlem1  23339  iblabslem  23344  iblabs  23345  iblabsr  23346  iblmulc2  23347  itgmulc2lem1  23348  bddmulibl  23355  itggt0  23358  itgcn  23359  ellimc2  23391  limcmpt  23397  limcres  23400  limccnp  23405  limccnp2  23406  limcco  23407  perfdvf  23417  dvreslem  23423  dvcnp2  23433  dvaddbr  23451  dvmulbr  23452  dvcjbr  23462  dvexp  23466  dvrec  23468  dvmptres3  23469  dvmptadd  23473  dvmptmul  23474  dvmptres2  23475  dvmptcmul  23477  dvmptcj  23481  dvmptntr  23484  dvmptco  23485  dvcnvlem  23487  dvef  23491  dvferm1  23496  dvferm2  23498  rolle  23501  dvlipcn  23505  dvle  23518  dvivthlem1  23519  dvivth  23521  lhop1lem  23524  lhop1  23525  lhop2  23526  lhop  23527  dvfsumle  23532  dvfsumge  23533  dvmptrecl  23535  dvfsumrlimf  23536  dvfsumlem2  23538  dvfsumlem3  23539  ftc1lem2  23547  ftc1lem6  23552  itgsubstlem  23559  tdeglem1  23566  tdeglem4  23568  coe1mul3  23607  elply2  23700  plyf  23702  elplyd  23706  plypf1  23716  coeeq2  23746  coemullem  23754  coe1termlem  23762  dvply2g  23788  elqaalem2  23823  taylfvallem  23860  taylf  23863  tayl0  23864  taylpfval  23867  taylpf  23868  taylthlem1  23875  taylthlem2  23876  ulmshftlem  23891  ulmshft  23892  ulmcau  23897  ulmss  23899  ulmdvlem1  23902  ulmdvlem3  23904  mtest  23906  mtestbdd  23907  itgulm2  23911  psergf  23914  radcnvlem1  23915  dvradcnv  23923  pserulm  23924  psercn2  23925  pserdvlem2  23930  abelthlem4  23936  abelthlem9  23942  pige3  24017  efif1olem4  24039  logtayl  24150  logccv  24153  loglesqrt  24243  logbf  24271  leibpi  24413  rlimcnp  24436  rlimcnp2  24437  xrlimcnp  24439  efrlim  24440  dfef2  24441  o1cxp  24445  cxp2lim  24447  amgmlem  24460  lgamgulmlem2  24500  lgamgulmlem6  24504  lgamcvg2  24525  gamcvg  24526  regamcl  24531  relgamcl  24532  basellem2  24552  basellem4  24554  basellem7  24557  basellem9  24559  sqff1o  24652  fsumvma  24682  dchrelbasd  24708  lgsfcl2  24772  lgsqrlem2  24816  lgseisenlem1  24844  lgseisenlem3  24846  lgseisenlem4  24847  chpo1ub  24913  dchrmusum2  24927  dchrvmasumiflem1  24934  dchrisum0ff  24940  dchrisum0lem1b  24948  dchrisum0lem2a  24950  logsqvma2  24976  pnt2  25046  pnt  25047  abvcxp  25048  padicabv  25063  lmif  25422  axlowdimlem15  25581  nbgraf1olem2  25764  wlkiswwlk2lem5  26016  wlknwwlknfun  26031  wlkiswwlkfun  26038  wwlkextfun  26050  clwlkisclwwlklem2a  26106  clwwlkf  26115  clwlkfclwwlk  26164  vdgrf  26218  vdgrfif  26219  frgrancvvdeqlem5  26354  numclwlk1lem2f  26412  numclwlk2lem2f  26423  ipblnfi  26888  ubthlem1  26903  minvecolem1  26907  htthlem  26951  hlimadd  27227  chscllem1  27673  hoaddcl  27794  homulcl  27795  brafn  27983  kbop  27989  cnlnadjlem2  28104  strlem3a  28288  hstrlem3a  28296  off2  28616  xppreima2  28623  fpwrelmap  28689  gsummpt2d  28905  gsumvsca1  28906  gsumvsca2  28907  xrge0tsmsd  28909  ordtrestNEW  29088  xrge0mulc1cn  29108  esumf1o  29232  esumadd  29239  esumcst  29245  esumpfinval  29257  esumpcvgval  29260  esumcvg  29268  esumsup  29271  measinb  29404  measdivcst  29408  mbfmco2  29447  sitgclg  29524  eulerpartlems  29542  dstfrvclim1  29659  gsumncl  29734  gsumnunsn  29735  erdszelem9  30228  indispcon  30263  cvxpcon  30271  cvmsss2  30303  cvmliftlem6  30319  cvmliftlem8  30321  cvmlift3lem3  30350  mrsubcv  30454  mrsubff  30456  mrsubrn  30457  mrsubccat  30462  elmrsubrn  30464  msubrn  30473  msubff  30474  mvhf  30502  divcnvlin  30664  iprodefisum  30673  faclimlem2  30676  faclim  30678  faclim2  30680  knoppcnlem5  31450  knoppcnlem8  31453  knoppcnlem10  31455  knoppcnlem11  31456  unbdqndv1  31462  knoppf  31489  curf  32340  finixpnum  32347  matunitlindflem1  32358  matunitlindflem2  32359  ptrest  32361  poimirlem17  32379  poimirlem20  32382  poimirlem24  32386  poimirlem30  32392  broucube  32396  mblfinlem2  32400  volsupnfl  32407  mbfposadd  32410  itg2addnclem2  32415  itg2gt0cn  32418  ibladdnclem  32419  itgaddnclem1  32421  itgaddnc  32423  iblabsnclem  32426  iblabsnc  32427  iblmulc2nc  32428  itgmulc2nclem1  32429  itgmulc2nclem2  32430  itgmulc2nc  32431  itgabsnc  32432  bddiblnc  32433  itggt0cn  32435  ftc1cnnc  32437  ftc1anclem1  32438  ftc1anclem2  32439  ftc1anclem3  32440  ftc1anclem4  32441  ftc1anclem5  32442  ftc1anclem6  32443  ftc1anclem7  32444  ftc1anclem8  32445  ftc1anc  32446  areacirclem4  32456  upixp  32477  totbndbnd  32541  prdsbnd  32545  cntotbnd  32548  rrnequiv  32587  lsatlss  33084  lflnegcl  33163  lshpkrcl  33204  tendoplcl  34870  tendo0cl  34879  tendoicl  34885  cmpfiiin  36061  mzpclall  36091  mzpindd  36110  fphpdo  36182  dnnumch3  36418  kelac1  36434  dfac21  36437  itgpowd  36602  rfovcnvf1od  37101  fsovfd  37109  fsovcnvlem  37110  clsk3nimkb  37141  expgrowth  37339  binomcxplemradcnv  37356  binomcxplemcvg  37358  binomcxplemnotnn0  37360  rnmptc  38131  mptelpm  38135  projf1o  38164  mapss2  38175  expcnfg  38441  clim1fr1  38451  mullimc  38466  ellimcabssub0  38467  mullimcf  38473  constlimc  38474  idlimc  38476  sumnnodd  38480  neglimc  38497  addlimc  38498  0ellimcdiv  38499  fnlimf  38528  cncfmptssg  38538  cncfshift  38542  cncfcompt  38551  icccncfext  38556  cncfiooiccre  38564  cxpcncf2  38569  fprodsubrecnncnvlem  38577  fprodaddrecnncnvlem  38579  dvsinax  38584  fperdvper  38591  dvmptresicc  38592  dvcosax  38599  ioodvbdlimc1lem1  38604  ioodvbdlimc1lem2  38605  ioodvbdlimc2lem  38607  dvnmptdivc  38611  dvnxpaek  38615  dvnprodlem1  38619  dvnprodlem2  38620  dvnprodlem3  38621  itgsinexplem1  38628  iblsplit  38641  itgcoscmulx  38644  itgiccshift  38655  itgperiod  38656  itgsbtaddcnst  38657  dirkerf  38773  dirkeritg  38778  dirkercncflem2  38780  fourierdlem4  38787  fourierdlem5  38788  fourierdlem9  38792  fourierdlem14  38797  fourierdlem16  38799  fourierdlem17  38800  fourierdlem18  38801  fourierdlem21  38804  fourierdlem22  38805  fourierdlem37  38820  fourierdlem50  38832  fourierdlem51  38833  fourierdlem53  38835  fourierdlem55  38837  fourierdlem57  38839  fourierdlem58  38840  fourierdlem59  38841  fourierdlem60  38842  fourierdlem61  38843  fourierdlem67  38849  fourierdlem68  38850  fourierdlem72  38854  fourierdlem73  38855  fourierdlem74  38856  fourierdlem75  38857  fourierdlem76  38858  fourierdlem78  38860  fourierdlem80  38862  fourierdlem81  38863  fourierdlem83  38865  fourierdlem84  38866  fourierdlem88  38870  fourierdlem92  38874  fourierdlem93  38875  fourierdlem97  38879  fourierdlem101  38883  fourierdlem103  38885  fourierdlem104  38886  fourierdlem111  38893  sqwvfoura  38904  elaa2lem  38909  etransclem1  38911  etransclem8  38918  etransclem20  38930  etransclem33  38943  etransclem35  38945  etransclem39  38949  rrxtopnfi  38965  ioorrnopnxrlem  38985  sge0tsms  39056  sge0snmpt  39059  sge0fsummpt  39066  sge0pr  39070  sge0lessmpt  39075  sge0iunmptlemfi  39089  sge0iunmptlemre  39091  sge0iunmpt  39094  sge0rpcpnf  39097  sge0isum  39103  nnfoctbdjlem  39131  psmeasure  39147  voliunsge0lem  39148  meaiuninclem  39156  meaiininclem  39159  omeiunltfirp  39192  carageniuncllem2  39195  caratheodorylem1  39199  caratheodorylem2  39200  isomenndlem  39203  hoicvr  39221  hoicvrrex  39229  ovnsupge0  39230  ovnlecvr  39231  ovnf  39236  ovn0lem  39238  ovnsubaddlem1  39243  ovnsubadd  39245  hsphoif  39249  sge0hsphoire  39262  hoidmv1lelem1  39264  hoidmv1lelem2  39265  hoidmv1lelem3  39266  hoidmv1le  39267  hoidmvlelem1  39268  hoidmvlelem2  39269  hoidmvlelem3  39270  hoidmvlelem5  39272  ovnhoilem1  39274  ovnhoilem2  39275  ovnlecvr2  39283  ovncvr2  39284  hoidifhspf  39291  hspmbllem2  39300  opnvonmbllem2  39306  ovnsubadd2lem  39318  ovolval4lem1  39322  ovolval4lem2  39323  ovolval5lem2  39326  ovnovollem1  39329  ovnovollem2  39330  iccvonmbllem  39352  vonioolem1  39354  vonioolem2  39355  vonicclem1  39357  vonicclem2  39358  smfid  39422  smfmbfcex  39429  smflim  39446  nsssmfmbflem  39447  smfmullem4  39462  fmtnodvds  39778  pfxf  40036  incistruhgr  40286  vtxdgf  40667  crctcsh1wlkn0  41005  1wlkiswwlks2lem5  41051  1wlkpwwlkf1ouspgr  41057  wlknwwlksnfun  41066  wlkwwlkfun  41073  wwlksnextfun  41085  clwlkclwwlklem2a  41188  clwwlksf  41203  clwlksfclwwlk  41250  frgrncvvdeqlem5  41454  av-numclwlk1lem2f  41503  av-numclwlk2lem2f  41514  c0mgm  41680  c0mhm  41681  c0snmgmhm  41685  funcringcsetcALTV2lem3  41811  funcringcsetclem3ALTV  41834  gsumlsscl  41939  ply1mulgsum  41953  lincfsuppcl  41977  linccl  41978  lincvalsc0  41985  lcoc0  41986  linc0scn0  41987  linc1  41989  lincsum  41993  lincscm  41994  lincscmcl  41996  lcoss  42000  lincext1  42018  el0ldep  42030  lincresunit1  42041  lincresunit3  42045  lmod1zr  42057  fdivmptf  42114  refdivmptf  42115  aacllem  42298  amgmwlem  42299  amgmlemALT  42300
  Copyright terms: Public domain W3C validator