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

Theorem fmptd 6536
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 3092 . 2 (𝜑 → ∀𝑥𝐴 𝐵𝐶)
3 fmptd.2 . . 3 𝐹 = (𝑥𝐴𝐵)
43fmpt 6532 . 2 (∀𝑥𝐴 𝐵𝐶𝐹:𝐴𝐶)
52, 4sylib 208 1 (𝜑𝐹:𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1620  wcel 2127  wral 3038  cmpt 4869  wf 6033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pr 5043
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-sbc 3565  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-opab 4853  df-mpt 4870  df-id 5162  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-fv 6045
This theorem is referenced by:  fmpt3d  6537  fliftrel  6709  off  7065  caofinvl  7077  curry1f  7427  curry2f  7429  fnwelem  7448  fdiagfn  8055  resixpfo  8100  pw2f1olem  8217  mapxpen  8279  xpmapenlem  8280  unxpdomlem3  8319  fsuppmptdm  8439  fsuppmptif  8458  wdom2d  8638  cantnfp1lem1  8736  cantnfp1lem2  8737  cantnfp1lem3  8738  cantnflem1d  8746  cantnflem1  8747  cantnf  8751  fseqenlem1  9008  fseqenlem2  9009  dfac8clem  9016  ac5num  9020  acni2  9030  infpwfien  9046  coftr  9258  fin23lem39  9335  isf34lem2  9358  fin1a2lem12  9396  axcc2lem  9421  axdc2lem  9433  axdc3lem4  9438  pwcfsdom  9568  canthp1lem2  9638  wuncval2  9732  gruf  9796  rpnnen1lem1  11979  rpnnen1lem1OLD  11985  monoord2  12997  seqf1o  13007  ccatcl  13517  swrdcl  13589  revcl  13681  revlen  13682  ello1mpt  14422  lo1o12  14434  lo1eq  14469  rlimeq  14470  climmpt2  14474  climrecl  14484  climge0  14485  o1compt  14488  rlimcn1b  14490  rlimdiv  14546  isercoll2  14569  caurcvg2  14578  caucvg  14579  sumrblem  14612  summolem2a  14616  fsumf1o  14624  sumss  14625  fsumss  14626  fsumcl2lem  14632  fsumadd  14640  isumclim3  14660  isummulc2  14663  fsummulc2  14686  fsumrelem  14709  climfsum  14722  isumshft  14741  divcnv  14755  supcvg  14758  prodfdiv  14798  prodrblem  14829  prodmolem2a  14834  fprodf1o  14846  prodss  14847  fprodss  14848  fprodser  14849  fprodcl2lem  14850  fprodmul  14860  fproddiv  14861  fprodn0  14879  iprodclim3  14901  fprodefsum  14995  rpnnen2lem2  15114  crth  15656  eulerthlem1  15659  iserodd  15713  prmreclem2  15794  prmreclem6  15798  1arithlem3  15802  4sqlem11  15832  vdwapf  15849  vdwlem2  15859  vdwlem4  15861  vdwlem6  15863  vdwlem10  15867  ramub1lem2  15904  ramcl  15906  prmodvdslcmf  15924  prmgaplcm  15937  prdsplusg  16291  prdsmulr  16292  prdsvsca  16293  mrcflem  16439  mreacs  16491  acsfn  16492  homaf  16852  funcestrcsetclem3  16954  funcsetcestrclem3  16968  prfcl  17015  curf1cl  17040  hofcllem  17070  hofcl  17071  yonedalem3a  17086  yonedalem4c  17089  yonedainv  17093  prdspjmhm  17539  pwsco1mhm  17542  pwsco2mhm  17543  gsumz  17546  gsumwspan  17555  vrmdfval  17565  vrmdf  17567  frmdup1  17573  grpinvf  17638  cycsubgcl  17792  cycsubgss  17793  conjghm  17863  conjnmz  17866  qusghm  17869  galactghm  17994  symgextf  18008  symgfixf  18027  pmtrf  18046  pmtrdifwrdellem1  18072  psgnunilem5  18085  odf1  18150  dfod2  18152  odf1o2  18159  pgpssslw  18200  sylow2blem1  18206  pj1f  18281  frgpmhm  18349  vrgpf  18352  mulgmhm  18404  mulgghm  18405  iscyggen2  18454  cyggenod  18457  iscyg3  18459  gsummptfsadd  18495  gsumzsplit  18498  gsumsplit2  18500  gsummptfidmsplitres  18502  gsumconst  18505  gsummptshft  18507  gsummhm2  18510  gsummptmhm  18511  gsummptfidminv  18518  gsummptfssub  18520  gsumzunsnd  18526  gsummptf1o  18533  gsummpt1n0  18535  gsum2dlem1  18540  gsum2dlem2  18541  gsum2d  18542  prdsgsum  18548  dprdfeq0  18592  dprdlub  18596  dprdz  18600  dprd2dlem1  18611  dprd2da  18612  ablfac1b  18640  ablfac2  18659  srglmhm  18706  srgrmhm  18707  ringlghm  18775  ringrghm  18776  gsumdixp  18780  abvtrivd  19013  issrngd  19034  lmodvsghm  19097  lspf  19147  pwssplit0  19231  asclf  19510  snifpsrbag  19539  psrass1lem  19550  psrmulcllem  19560  psr1cl  19575  psrlidm  19576  psrridm  19577  psrcom  19582  resspsrmul  19590  subrgpsr  19592  mvrf  19597  mplmon  19636  mplmonmul  19637  mplcoe1  19638  mplcoe5lem  19640  mplcoe5  19641  mplbas2  19643  psrbagsn  19668  evlslem4  19681  evlslem2  19685  evlslem6  19686  evlslem3  19687  evlslem1  19688  evlsval2  19693  psropprmul  19781  coe1mul2  19812  coe1tmmul2  19819  coe1tmmul  19820  ply1coe  19839  gsumsmonply1  19846  gsummoncoe1  19847  gsumfsum  19986  regsumfsum  19987  expmhm  19988  expghm  20017  mulgghm2  20018  evpmodpmf1o  20115  isphld  20172  pjff  20229  frlmgsum  20284  frlmsplit2  20285  frlmphl  20293  uvcff  20303  uvcresum  20305  frlmup1  20310  mamulid  20420  mamurid  20421  scmatf  20508  mdetf  20574  mdetunilem9  20599  mdetuni0  20600  mdetmul  20602  maduf  20620  smadiadetlem3lem1  20645  cpm2mf  20730  m2cpmfo  20734  pmatcollpw1  20754  pmatcollpw3lem  20761  pmatcollpw3fi1lem1  20764  pmatcollpw3fi1lem2  20765  pm2mpcl  20775  mply1topmatcl  20783  mp2pm2mplem2  20785  mp2pm2mp  20789  pm2mpmhmlem2  20797  chfacfisf  20832  chfacfisfcpmat  20833  cpmidpmatlem2  20849  cayhamlem4  20866  pptbas  20985  tgrest  21136  resttopon  21138  rest0  21146  restfpw  21156  ordtbaslem  21165  ordtuni  21167  ordtrest  21179  cnpfval  21211  pnrmopn  21320  cncmp  21368  discmp  21374  1stcfb  21421  2ndcomap  21434  dis2ndc  21436  lly1stc  21472  comppfsc  21508  kgencmp  21521  ptpjpre1  21547  ptpjcn  21587  ptcldmpt  21590  ptclsg  21591  dfac14  21594  xkoccn  21595  txcnp  21596  ptcnp  21598  txcnmpt  21600  uptx  21601  ptcn  21603  ptrescn  21615  txlm  21624  xkoptsub  21630  xkoco1cn  21633  xkoco2cn  21634  cnmpt11  21639  xkoinjcn  21663  kqffn  21701  pt1hmeo  21782  fbasrn  21860  trfilss  21865  trfg  21867  rnelfmlem  21928  txflf  21982  flfcnp2  21983  fclscmpi  22005  alexsublem  22020  ptcmplem3  22030  symgtgp  22077  subgntr  22082  opnsubg  22083  clsnsg  22085  tgpconncomp  22088  tsmsfbas  22103  eltsms  22108  haustsms  22111  tsmscls  22113  tsms0  22117  tsmsmhm  22121  tgptsmscls  22125  tsmssplit  22127  tsmsxplem1  22128  tsmsxplem2  22129  ustuqtop0  22216  prdsdsf  22344  prdsxmetlem  22345  imasdsf1olem  22350  prdsbl  22468  stdbdxmet  22492  met1stc  22498  nmf2  22569  xrge0gsumle  22808  xrge0tsms  22809  metdsf  22823  metdsge  22824  mulc1cncf  22880  cncfmpt2ss  22890  cnmptre  22898  evth  22930  evth2  22931  lebnumlem1  22932  cphnmf  23166  tchcph  23207  cmetcaulem  23257  rrxmval  23359  minveclem1  23366  minveclem3b  23370  ovollb2lem  23427  ovolctb  23429  ovolunlem1a  23435  ovolunlem1  23436  ovoliunlem1  23441  ovoliunlem2  23442  ovoliun  23444  ovolshftlem1  23448  ovolscalem1  23452  ovolicc1  23455  iunmbl  23492  ioombl1lem1  23497  uniioombllem2  23522  uniioombllem3  23524  volsup2  23544  volcn  23545  vitalilem4  23550  vitalilem5  23551  mbfconst  23572  ismbfcn2  23576  mbfeqalem  23579  mbfss  23583  mbfmulc2re  23585  mbfmax  23586  mbfneg  23587  mbfpos  23588  mbfposr  23589  mbfposb  23590  mbfadd  23598  mbfmulc2  23600  mbfsup  23601  mbfinf  23602  mbflimsup  23603  mbflimlem  23604  mbflim  23605  i1f1lem  23626  i1f1  23627  i1fres  23642  itg1climres  23651  mbfi1fseqlem3  23654  mbfi1fseqlem4  23655  mbfi1flimlem  23659  mbfi1flim  23660  mbfmullem2  23661  mbfmul  23663  itg2const2  23678  itg2seq  23679  itg2splitlem  23685  itg2split  23686  itg2monolem1  23687  itg2monolem2  23688  itg2monolem3  23689  itg2mono  23690  itg2i1fseq  23692  itg2i1fseq2  23693  itg2gt0  23697  itg2cnlem1  23698  itg2cnlem2  23699  itg2cn  23700  iblss  23741  itgitg1  23745  itgle  23746  itgeqa  23750  itgss3  23751  ibladdlem  23756  itgaddlem1  23759  iblabslem  23764  iblabs  23765  iblabsr  23766  iblmulc2  23767  itgmulc2lem1  23768  bddmulibl  23775  itggt0  23778  itgcn  23779  ellimc2  23811  limcmpt  23817  limcres  23820  limccnp  23825  limccnp2  23826  limcco  23827  perfdvf  23837  dvreslem  23843  dvcnp2  23853  dvaddbr  23871  dvmulbr  23872  dvcjbr  23882  dvexp  23886  dvrec  23888  dvmptres3  23889  dvmptadd  23893  dvmptmul  23894  dvmptres2  23895  dvmptcmul  23897  dvmptcj  23901  dvmptntr  23904  dvmptco  23905  dvcnvlem  23909  dvef  23913  dvferm1  23918  dvferm2  23920  rolle  23923  dvlipcn  23927  dvle  23940  dvivthlem1  23941  dvivth  23943  lhop1lem  23946  lhop1  23947  lhop2  23948  lhop  23949  dvfsumle  23954  dvfsumge  23955  dvmptrecl  23957  dvfsumrlimf  23958  dvfsumlem2  23960  dvfsumlem3  23961  ftc1lem2  23969  ftc1lem6  23974  itgsubstlem  23981  tdeglem1  23988  tdeglem4  23990  coe1mul3  24029  elply2  24122  plyf  24124  elplyd  24128  plypf1  24138  coeeq2  24168  coemullem  24176  coe1termlem  24184  dvply2g  24210  elqaalem2  24245  taylfvallem  24282  taylf  24285  tayl0  24286  taylpfval  24289  taylpf  24290  taylthlem1  24297  taylthlem2  24298  ulmshftlem  24313  ulmshft  24314  ulmcau  24319  ulmss  24321  ulmdvlem1  24324  ulmdvlem3  24326  mtest  24328  mtestbdd  24329  itgulm2  24333  psergf  24336  radcnvlem1  24337  dvradcnv  24345  pserulm  24346  psercn2  24347  pserdvlem2  24352  abelthlem4  24358  abelthlem9  24364  pige3  24439  efif1olem4  24461  logtayl  24576  logccv  24579  loglesqrt  24669  logbf  24697  leibpi  24839  rlimcnp  24862  rlimcnp2  24863  xrlimcnp  24865  efrlim  24866  dfef2  24867  o1cxp  24871  cxp2lim  24873  amgmlem  24886  lgamgulmlem2  24926  lgamgulmlem6  24930  lgamcvg2  24951  gamcvg  24952  regamcl  24957  relgamcl  24958  basellem2  24978  basellem4  24980  basellem7  24983  basellem9  24985  sqff1o  25078  fsumvma  25108  dchrelbasd  25134  lgsfcl2  25198  lgsqrlem2  25242  lgseisenlem1  25270  lgseisenlem3  25272  lgseisenlem4  25273  chpo1ub  25339  dchrmusum2  25353  dchrvmasumiflem1  25360  dchrisum0ff  25366  dchrisum0lem1b  25374  dchrisum0lem2a  25376  logsqvma2  25402  pnt2  25472  pnt  25473  abvcxp  25474  padicabv  25489  lmif  25847  axlowdimlem15  26006  incistruhgr  26144  vtxdgf  26548  crctcshwlkn0  26895  wlkiswwlks2lem5  26953  wlkpwwlkf1ouspgr  26959  wlknwwlksnfun  26968  wlkwwlkfun  26975  wwlksnextfun  26987  clwlkclwwlklem2a  27092  clwlkclwwlkf  27102  clwwlkf  27147  clwlksfclwwlkOLD  27187  frgrncvvdeqlem4  27427  numclwlk1lem2f  27485  numclwlk2lem2f  27509  numclwlk2lem2fOLD  27516  ipblnfi  27991  ubthlem1  28006  minvecolem1  28010  htthlem  28054  hlimadd  28330  chscllem1  28776  hoaddcl  28897  homulcl  28898  brafn  29086  kbop  29092  cnlnadjlem2  29207  strlem3a  29391  hstrlem3a  29399  off2  29723  xppreima2  29730  fpwrelmap  29788  gsummpt2d  30061  gsumvsca1  30062  gsumvsca2  30063  xrge0tsmsd  30065  ordtrestNEW  30247  xrge0mulc1cn  30267  esumf1o  30392  esumadd  30399  esumcst  30405  esumpfinval  30417  esumpcvgval  30420  esumcvg  30428  esumsup  30431  measinb  30564  measdivcst  30568  mbfmco2  30607  sitgclg  30684  eulerpartlems  30702  dstfrvclim1  30819  gsumncl  30894  gsumnunsn  30895  fdvneggt  30958  fdvnegge  30960  itgexpif  30964  logdivsqrle  31008  erdszelem9  31459  indispconn  31494  cvxpconn  31502  cvmsss2  31534  cvmliftlem6  31550  cvmliftlem8  31552  cvmlift3lem3  31581  mrsubcv  31685  mrsubff  31687  mrsubrn  31688  mrsubccat  31693  elmrsubrn  31695  msubrn  31704  msubff  31705  mvhf  31733  divcnvlin  31896  iprodefisum  31905  faclimlem2  31908  faclim  31910  faclim2  31912  knoppcnlem5  32764  knoppcnlem8  32767  knoppcnlem10  32769  knoppcnlem11  32770  unbdqndv1  32776  knoppf  32803  curf  33669  finixpnum  33676  matunitlindflem1  33687  matunitlindflem2  33688  ptrest  33690  poimirlem17  33708  poimirlem20  33711  poimirlem24  33715  poimirlem30  33721  broucube  33725  mblfinlem2  33729  volsupnfl  33736  mbfposadd  33739  itg2addnclem2  33744  itg2gt0cn  33747  ibladdnclem  33748  itgaddnclem1  33750  itgaddnc  33752  iblabsnclem  33755  iblabsnc  33756  iblmulc2nc  33757  itgmulc2nclem1  33758  itgmulc2nclem2  33759  itgmulc2nc  33760  itgabsnc  33761  bddiblnc  33762  itggt0cn  33764  ftc1cnnc  33766  ftc1anclem1  33767  ftc1anclem2  33768  ftc1anclem3  33769  ftc1anclem4  33770  ftc1anclem5  33771  ftc1anclem6  33772  ftc1anclem7  33773  ftc1anclem8  33774  ftc1anc  33775  areacirclem4  33785  upixp  33806  totbndbnd  33870  prdsbnd  33874  cntotbnd  33877  rrnequiv  33916  lsatlss  34755  lflnegcl  34834  lshpkrcl  34875  tendoplcl  36540  tendo0cl  36549  tendoicl  36555  cmpfiiin  37731  mzpclall  37761  mzpindd  37780  fphpdo  37852  dnnumch3  38088  kelac1  38104  dfac21  38107  itgpowd  38271  rfovcnvf1od  38769  fsovfd  38777  fsovcnvlem  38778  clsk3nimkb  38809  expgrowth  39005  binomcxplemradcnv  39022  binomcxplemcvg  39024  binomcxplemnotnn0  39026  rnmptc  39821  mptelpm  39825  projf1o  39854  mapss2  39865  monoord2xrv  40181  expcnfg  40295  clim1fr1  40305  mullimc  40320  ellimcabssub0  40321  mullimcf  40327  constlimc  40328  idlimc  40330  sumnnodd  40334  neglimc  40351  addlimc  40352  0ellimcdiv  40353  fnlimf  40382  limsupvaluz2  40442  supcnvlimsup  40444  climliminflimsupd  40505  cncfmptssg  40555  cncfshift  40559  cncfcompt  40568  icccncfext  40572  cncfiooiccre  40580  cxpcncf2  40585  fprodsubrecnncnvlem  40593  fprodaddrecnncnvlem  40595  dvsinax  40599  fperdvper  40605  dvmptresicc  40606  dvcosax  40613  ioodvbdlimc1lem1  40618  ioodvbdlimc1lem2  40619  ioodvbdlimc2lem  40621  dvnmptdivc  40625  dvnxpaek  40629  dvnprodlem1  40633  dvnprodlem2  40634  dvnprodlem3  40635  itgsinexplem1  40641  iblsplit  40654  itgcoscmulx  40657  itgiccshift  40668  itgperiod  40669  itgsbtaddcnst  40670  dirkerf  40786  dirkeritg  40791  dirkercncflem2  40793  fourierdlem4  40800  fourierdlem5  40801  fourierdlem9  40805  fourierdlem14  40810  fourierdlem16  40812  fourierdlem17  40813  fourierdlem18  40814  fourierdlem21  40817  fourierdlem22  40818  fourierdlem37  40833  fourierdlem50  40845  fourierdlem51  40846  fourierdlem53  40848  fourierdlem55  40850  fourierdlem57  40852  fourierdlem58  40853  fourierdlem59  40854  fourierdlem60  40855  fourierdlem61  40856  fourierdlem67  40862  fourierdlem68  40863  fourierdlem72  40867  fourierdlem73  40868  fourierdlem74  40869  fourierdlem75  40870  fourierdlem76  40871  fourierdlem78  40873  fourierdlem80  40875  fourierdlem81  40876  fourierdlem83  40878  fourierdlem84  40879  fourierdlem88  40883  fourierdlem92  40887  fourierdlem93  40888  fourierdlem97  40892  fourierdlem101  40896  fourierdlem103  40898  fourierdlem104  40899  fourierdlem111  40906  sqwvfoura  40917  elaa2lem  40922  etransclem1  40924  etransclem8  40931  etransclem20  40943  etransclem33  40956  etransclem35  40958  etransclem39  40962  rrxtopnfi  40978  ioorrnopnxrlem  40998  sge0tsms  41069  sge0snmpt  41072  sge0fsummpt  41079  sge0pr  41083  sge0lessmpt  41088  sge0iunmptlemfi  41102  sge0iunmptlemre  41104  sge0iunmpt  41107  sge0rpcpnf  41110  sge0isum  41116  nnfoctbdjlem  41144  psmeasure  41160  voliunsge0lem  41161  meaiuninclem  41169  meaiuninc3v  41173  meaiininclem  41175  omeiunltfirp  41208  carageniuncllem2  41211  caratheodorylem1  41215  caratheodorylem2  41216  isomenndlem  41219  hoicvr  41237  hoicvrrex  41245  ovnsupge0  41246  ovnlecvr  41247  ovnf  41252  ovn0lem  41254  ovnsubaddlem1  41259  ovnsubadd  41261  hsphoif  41265  sge0hsphoire  41278  hoidmv1lelem1  41280  hoidmv1lelem2  41281  hoidmv1lelem3  41282  hoidmv1le  41283  hoidmvlelem1  41284  hoidmvlelem2  41285  hoidmvlelem3  41286  hoidmvlelem5  41288  ovnhoilem1  41290  ovnhoilem2  41291  ovnlecvr2  41299  ovncvr2  41300  hoidifhspf  41307  hspmbllem2  41316  opnvonmbllem2  41322  ovnsubadd2lem  41334  ovolval4lem1  41338  ovolval4lem2  41339  ovolval5lem2  41342  ovnovollem1  41345  ovnovollem2  41346  iccvonmbllem  41367  vonioolem1  41369  vonioolem2  41370  vonicclem1  41372  vonicclem2  41373  smfid  41436  smfmbfcex  41443  smflim  41460  nsssmfmbflem  41461  smfmullem4  41476  smfsuplem1  41492  smfsuplem3  41494  smflimsuplem3  41503  pfxf  41868  fmtnodvds  41935  c0mgm  42388  c0mhm  42389  c0snmgmhm  42393  funcringcsetcALTV2lem3  42517  funcringcsetclem3ALTV  42540  gsumlsscl  42643  ply1mulgsum  42657  lincfsuppcl  42681  linccl  42682  lincvalsc0  42689  lcoc0  42690  linc0scn0  42691  linc1  42693  lincsum  42697  lincscm  42698  lincscmcl  42700  lcoss  42704  lincext1  42722  el0ldep  42734  lincresunit1  42745  lincresunit3  42749  lmod1zr  42761  fdivmptf  42814  refdivmptf  42815  aacllem  43029  amgmwlem  43030  amgmlemALT  43031
  Copyright terms: Public domain W3C validator