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

Theorem fmptd 6425
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 2995 . 2 (𝜑 → ∀𝑥𝐴 𝐵𝐶)
3 fmptd.2 . . 3 𝐹 = (𝑥𝐴𝐵)
43fmpt 6421 . 2 (∀𝑥𝐴 𝐵𝐶𝐹:𝐴𝐶)
52, 4sylib 208 1 (𝜑𝐹:𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wcel 2030  wral 2941  cmpt 4762  wf 5922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934
This theorem is referenced by:  fmpt3d  6426  fliftrel  6598  off  6954  caofinvl  6966  curry1f  7316  curry2f  7318  fnwelem  7337  fdiagfn  7943  resixpfo  7988  pw2f1olem  8105  mapxpen  8167  xpmapenlem  8168  unxpdomlem3  8207  fsuppmptdm  8327  fsuppmptif  8346  wdom2d  8526  cantnfp1lem1  8613  cantnfp1lem2  8614  cantnfp1lem3  8615  cantnflem1d  8623  cantnflem1  8624  cantnf  8628  fseqenlem1  8885  fseqenlem2  8886  dfac8clem  8893  ac5num  8897  acni2  8907  infpwfien  8923  coftr  9133  fin23lem39  9210  isf34lem2  9233  fin1a2lem12  9271  axcc2lem  9296  axdc2lem  9308  axdc3lem4  9313  pwcfsdom  9443  canthp1lem2  9513  wuncval2  9607  gruf  9671  rpnnen1lem1  11853  rpnnen1lem1OLD  11859  monoord2  12872  seqf1o  12882  ccatcl  13392  swrdcl  13464  revcl  13556  revlen  13557  ello1mpt  14296  lo1o12  14308  lo1eq  14343  rlimeq  14344  climmpt2  14348  climrecl  14358  climge0  14359  o1compt  14362  rlimcn1b  14364  rlimdiv  14420  isercoll2  14443  caurcvg2  14452  caucvg  14453  sumrblem  14486  summolem2a  14490  fsumf1o  14498  sumss  14499  fsumss  14500  fsumcl2lem  14506  fsumadd  14514  isumclim3  14534  isummulc2  14537  fsummulc2  14560  fsumrelem  14583  climfsum  14596  isumshft  14615  divcnv  14629  supcvg  14632  prodfdiv  14672  prodrblem  14703  prodmolem2a  14708  fprodf1o  14720  prodss  14721  fprodss  14722  fprodser  14723  fprodcl2lem  14724  fprodmul  14734  fproddiv  14735  fprodn0  14753  iprodclim3  14775  fprodefsum  14869  rpnnen2lem2  14988  crth  15530  eulerthlem1  15533  iserodd  15587  prmreclem2  15668  prmreclem6  15672  1arithlem3  15676  4sqlem11  15706  vdwapf  15723  vdwlem2  15733  vdwlem4  15735  vdwlem6  15737  vdwlem10  15741  ramub1lem2  15778  ramcl  15780  prmodvdslcmf  15798  prmgaplcm  15811  prdsplusg  16165  prdsmulr  16166  prdsvsca  16167  mrcflem  16313  mreacs  16366  acsfn  16367  homaf  16727  funcestrcsetclem3  16829  funcsetcestrclem3  16843  prfcl  16890  curf1cl  16915  hofcllem  16945  hofcl  16946  yonedalem3a  16961  yonedalem4c  16964  yonedainv  16968  prdspjmhm  17414  pwsco1mhm  17417  pwsco2mhm  17418  gsumz  17421  gsumwspan  17430  vrmdfval  17440  vrmdf  17442  frmdup1  17448  grpinvf  17513  cycsubgcl  17667  cycsubgss  17668  conjghm  17738  conjnmz  17741  qusghm  17744  galactghm  17869  symgextf  17883  symgfixf  17902  pmtrf  17921  pmtrdifwrdellem1  17947  psgnunilem5  17960  odf1  18025  dfod2  18027  odf1o2  18034  pgpssslw  18075  sylow2blem1  18081  pj1f  18156  frgpmhm  18224  vrgpf  18227  mulgmhm  18279  mulgghm  18280  iscyggen2  18329  cyggenod  18332  iscyg3  18334  gsummptfsadd  18370  gsumzsplit  18373  gsumsplit2  18375  gsummptfidmsplitres  18377  gsumconst  18380  gsummptshft  18382  gsummhm2  18385  gsummptmhm  18386  gsummptfidminv  18393  gsummptfssub  18395  gsumzunsnd  18401  gsummptf1o  18408  gsummpt1n0  18410  gsum2dlem1  18415  gsum2dlem2  18416  gsum2d  18417  prdsgsum  18423  dprdfeq0  18467  dprdlub  18471  dprdz  18475  dprd2dlem1  18486  dprd2da  18487  ablfac1b  18515  ablfac2  18534  srglmhm  18581  srgrmhm  18582  ringlghm  18650  ringrghm  18651  gsumdixp  18655  abvtrivd  18888  issrngd  18909  lmodvsghm  18972  lspf  19022  pwssplit0  19106  asclf  19385  snifpsrbag  19414  psrass1lem  19425  psrmulcllem  19435  psr1cl  19450  psrlidm  19451  psrridm  19452  psrcom  19457  resspsrmul  19465  subrgpsr  19467  mvrf  19472  mplmon  19511  mplmonmul  19512  mplcoe1  19513  mplcoe5lem  19515  mplcoe5  19516  mplbas2  19518  psrbagsn  19543  evlslem4  19556  evlslem2  19560  evlslem6  19561  evlslem3  19562  evlslem1  19563  evlsval2  19568  psropprmul  19656  coe1mul2  19687  coe1tmmul2  19694  coe1tmmul  19695  ply1coe  19714  gsumsmonply1  19721  gsummoncoe1  19722  gsumfsum  19861  regsumfsum  19862  expmhm  19863  expghm  19892  mulgghm2  19893  evpmodpmf1o  19990  isphld  20047  pjff  20104  frlmgsum  20159  frlmsplit2  20160  frlmphl  20168  uvcff  20178  uvcresum  20180  frlmup1  20185  mamulid  20295  mamurid  20296  scmatf  20383  mdetf  20449  mdetunilem9  20474  mdetuni0  20475  mdetmul  20477  maduf  20495  smadiadetlem3lem1  20520  cpm2mf  20605  m2cpmfo  20609  pmatcollpw1  20629  pmatcollpw3lem  20636  pmatcollpw3fi1lem1  20639  pmatcollpw3fi1lem2  20640  pm2mpcl  20650  mply1topmatcl  20658  mp2pm2mplem2  20660  mp2pm2mp  20664  pm2mpmhmlem2  20672  chfacfisf  20707  chfacfisfcpmat  20708  cpmidpmatlem2  20724  cayhamlem4  20741  pptbas  20860  tgrest  21011  resttopon  21013  rest0  21021  restfpw  21031  ordtbaslem  21040  ordtuni  21042  ordtrest  21054  cnpfval  21086  pnrmopn  21195  cncmp  21243  discmp  21249  1stcfb  21296  2ndcomap  21309  dis2ndc  21311  lly1stc  21347  comppfsc  21383  kgencmp  21396  ptpjpre1  21422  ptpjcn  21462  ptcldmpt  21465  ptclsg  21466  dfac14  21469  xkoccn  21470  txcnp  21471  ptcnp  21473  txcnmpt  21475  uptx  21476  ptcn  21478  ptrescn  21490  txlm  21499  xkoptsub  21505  xkoco1cn  21508  xkoco2cn  21509  cnmpt11  21514  xkoinjcn  21538  kqffn  21576  pt1hmeo  21657  fbasrn  21735  trfilss  21740  trfg  21742  rnelfmlem  21803  txflf  21857  flfcnp2  21858  fclscmpi  21880  alexsublem  21895  ptcmplem3  21905  symgtgp  21952  subgntr  21957  opnsubg  21958  clsnsg  21960  tgpconncomp  21963  tsmsfbas  21978  eltsms  21983  haustsms  21986  tsmscls  21988  tsms0  21992  tsmsmhm  21996  tgptsmscls  22000  tsmssplit  22002  tsmsxplem1  22003  tsmsxplem2  22004  ustuqtop0  22091  prdsdsf  22219  prdsxmetlem  22220  imasdsf1olem  22225  prdsbl  22343  stdbdxmet  22367  met1stc  22373  nmf2  22444  xrge0gsumle  22683  xrge0tsms  22684  metdsf  22698  metdsge  22699  mulc1cncf  22755  cncfmpt2ss  22765  cnmptre  22773  evth  22805  evth2  22806  lebnumlem1  22807  cphnmf  23041  tchcph  23082  cmetcaulem  23132  rrxmval  23234  minveclem1  23241  minveclem3b  23245  ovollb2lem  23302  ovolctb  23304  ovolunlem1a  23310  ovolunlem1  23311  ovoliunlem1  23316  ovoliunlem2  23317  ovoliun  23319  ovolshftlem1  23323  ovolscalem1  23327  ovolicc1  23330  iunmbl  23367  ioombl1lem1  23372  uniioombllem2  23397  uniioombllem3  23399  volsup2  23419  volcn  23420  vitalilem4  23425  vitalilem5  23426  mbfconst  23447  ismbfcn2  23451  mbfeqalem  23454  mbfss  23458  mbfmulc2re  23460  mbfmax  23461  mbfneg  23462  mbfpos  23463  mbfposr  23464  mbfposb  23465  mbfadd  23473  mbfmulc2  23475  mbfsup  23476  mbfinf  23477  mbflimsup  23478  mbflimlem  23479  mbflim  23480  i1f1lem  23501  i1f1  23502  i1fres  23517  itg1climres  23526  mbfi1fseqlem3  23529  mbfi1fseqlem4  23530  mbfi1flimlem  23534  mbfi1flim  23535  mbfmullem2  23536  mbfmul  23538  itg2const2  23553  itg2seq  23554  itg2splitlem  23560  itg2split  23561  itg2monolem1  23562  itg2monolem2  23563  itg2monolem3  23564  itg2mono  23565  itg2i1fseq  23567  itg2i1fseq2  23568  itg2gt0  23572  itg2cnlem1  23573  itg2cnlem2  23574  itg2cn  23575  iblss  23616  itgitg1  23620  itgle  23621  itgeqa  23625  itgss3  23626  ibladdlem  23631  itgaddlem1  23634  iblabslem  23639  iblabs  23640  iblabsr  23641  iblmulc2  23642  itgmulc2lem1  23643  bddmulibl  23650  itggt0  23653  itgcn  23654  ellimc2  23686  limcmpt  23692  limcres  23695  limccnp  23700  limccnp2  23701  limcco  23702  perfdvf  23712  dvreslem  23718  dvcnp2  23728  dvaddbr  23746  dvmulbr  23747  dvcjbr  23757  dvexp  23761  dvrec  23763  dvmptres3  23764  dvmptadd  23768  dvmptmul  23769  dvmptres2  23770  dvmptcmul  23772  dvmptcj  23776  dvmptntr  23779  dvmptco  23780  dvcnvlem  23784  dvef  23788  dvferm1  23793  dvferm2  23795  rolle  23798  dvlipcn  23802  dvle  23815  dvivthlem1  23816  dvivth  23818  lhop1lem  23821  lhop1  23822  lhop2  23823  lhop  23824  dvfsumle  23829  dvfsumge  23830  dvmptrecl  23832  dvfsumrlimf  23833  dvfsumlem2  23835  dvfsumlem3  23836  ftc1lem2  23844  ftc1lem6  23849  itgsubstlem  23856  tdeglem1  23863  tdeglem4  23865  coe1mul3  23904  elply2  23997  plyf  23999  elplyd  24003  plypf1  24013  coeeq2  24043  coemullem  24051  coe1termlem  24059  dvply2g  24085  elqaalem2  24120  taylfvallem  24157  taylf  24160  tayl0  24161  taylpfval  24164  taylpf  24165  taylthlem1  24172  taylthlem2  24173  ulmshftlem  24188  ulmshft  24189  ulmcau  24194  ulmss  24196  ulmdvlem1  24199  ulmdvlem3  24201  mtest  24203  mtestbdd  24204  itgulm2  24208  psergf  24211  radcnvlem1  24212  dvradcnv  24220  pserulm  24221  psercn2  24222  pserdvlem2  24227  abelthlem4  24233  abelthlem9  24239  pige3  24314  efif1olem4  24336  logtayl  24451  logccv  24454  loglesqrt  24544  logbf  24572  leibpi  24714  rlimcnp  24737  rlimcnp2  24738  xrlimcnp  24740  efrlim  24741  dfef2  24742  o1cxp  24746  cxp2lim  24748  amgmlem  24761  lgamgulmlem2  24801  lgamgulmlem6  24805  lgamcvg2  24826  gamcvg  24827  regamcl  24832  relgamcl  24833  basellem2  24853  basellem4  24855  basellem7  24858  basellem9  24860  sqff1o  24953  fsumvma  24983  dchrelbasd  25009  lgsfcl2  25073  lgsqrlem2  25117  lgseisenlem1  25145  lgseisenlem3  25147  lgseisenlem4  25148  chpo1ub  25214  dchrmusum2  25228  dchrvmasumiflem1  25235  dchrisum0ff  25241  dchrisum0lem1b  25249  dchrisum0lem2a  25251  logsqvma2  25277  pnt2  25347  pnt  25348  abvcxp  25349  padicabv  25364  lmif  25722  axlowdimlem15  25881  incistruhgr  26019  vtxdgf  26423  crctcshwlkn0  26769  wlkiswwlks2lem5  26827  wlkpwwlkf1ouspgr  26833  wlknwwlksnfun  26842  wlkwwlkfun  26849  wwlksnextfun  26861  clwlkclwwlklem2a  26964  clwwlkf  27010  clwlksfclwwlk  27049  frgrncvvdeqlem4  27282  numclwlk1lem2f  27345  numclwlk2lem2f  27357  numclwlk2lem2fOLD  27364  ipblnfi  27839  ubthlem1  27854  minvecolem1  27858  htthlem  27902  hlimadd  28178  chscllem1  28624  hoaddcl  28745  homulcl  28746  brafn  28934  kbop  28940  cnlnadjlem2  29055  strlem3a  29239  hstrlem3a  29247  off2  29571  xppreima2  29578  fpwrelmap  29636  gsummpt2d  29909  gsumvsca1  29910  gsumvsca2  29911  xrge0tsmsd  29913  ordtrestNEW  30095  xrge0mulc1cn  30115  esumf1o  30240  esumadd  30247  esumcst  30253  esumpfinval  30265  esumpcvgval  30268  esumcvg  30276  esumsup  30279  measinb  30412  measdivcst  30416  mbfmco2  30455  sitgclg  30532  eulerpartlems  30550  dstfrvclim1  30667  gsumncl  30742  gsumnunsn  30743  fdvneggt  30806  fdvnegge  30808  itgexpif  30812  logdivsqrle  30856  erdszelem9  31307  indispconn  31342  cvxpconn  31350  cvmsss2  31382  cvmliftlem6  31398  cvmliftlem8  31400  cvmlift3lem3  31429  mrsubcv  31533  mrsubff  31535  mrsubrn  31536  mrsubccat  31541  elmrsubrn  31543  msubrn  31552  msubff  31553  mvhf  31581  divcnvlin  31744  iprodefisum  31753  faclimlem2  31756  faclim  31758  faclim2  31760  knoppcnlem5  32612  knoppcnlem8  32615  knoppcnlem10  32617  knoppcnlem11  32618  unbdqndv1  32624  knoppf  32651  curf  33517  finixpnum  33524  matunitlindflem1  33535  matunitlindflem2  33536  ptrest  33538  poimirlem17  33556  poimirlem20  33559  poimirlem24  33563  poimirlem30  33569  broucube  33573  mblfinlem2  33577  volsupnfl  33584  mbfposadd  33587  itg2addnclem2  33592  itg2gt0cn  33595  ibladdnclem  33596  itgaddnclem1  33598  itgaddnc  33600  iblabsnclem  33603  iblabsnc  33604  iblmulc2nc  33605  itgmulc2nclem1  33606  itgmulc2nclem2  33607  itgmulc2nc  33608  itgabsnc  33609  bddiblnc  33610  itggt0cn  33612  ftc1cnnc  33614  ftc1anclem1  33615  ftc1anclem2  33616  ftc1anclem3  33617  ftc1anclem4  33618  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  areacirclem4  33633  upixp  33654  totbndbnd  33718  prdsbnd  33722  cntotbnd  33725  rrnequiv  33764  lsatlss  34601  lflnegcl  34680  lshpkrcl  34721  tendoplcl  36386  tendo0cl  36395  tendoicl  36401  cmpfiiin  37577  mzpclall  37607  mzpindd  37626  fphpdo  37698  dnnumch3  37934  kelac1  37950  dfac21  37953  itgpowd  38117  rfovcnvf1od  38615  fsovfd  38623  fsovcnvlem  38624  clsk3nimkb  38655  expgrowth  38851  binomcxplemradcnv  38868  binomcxplemcvg  38870  binomcxplemnotnn0  38872  rnmptc  39667  mptelpm  39671  projf1o  39700  mapss2  39711  monoord2xrv  40027  expcnfg  40141  clim1fr1  40151  mullimc  40166  ellimcabssub0  40167  mullimcf  40173  constlimc  40174  idlimc  40176  sumnnodd  40180  neglimc  40197  addlimc  40198  0ellimcdiv  40199  fnlimf  40228  limsupvaluz2  40288  supcnvlimsup  40290  climliminflimsupd  40351  cncfmptssg  40401  cncfshift  40405  cncfcompt  40414  icccncfext  40418  cncfiooiccre  40426  cxpcncf2  40431  fprodsubrecnncnvlem  40439  fprodaddrecnncnvlem  40441  dvsinax  40445  fperdvper  40451  dvmptresicc  40452  dvcosax  40459  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnmptdivc  40471  dvnxpaek  40475  dvnprodlem1  40479  dvnprodlem2  40480  dvnprodlem3  40481  itgsinexplem1  40487  iblsplit  40500  itgcoscmulx  40503  itgiccshift  40514  itgperiod  40515  itgsbtaddcnst  40516  dirkerf  40632  dirkeritg  40637  dirkercncflem2  40639  fourierdlem4  40646  fourierdlem5  40647  fourierdlem9  40651  fourierdlem14  40656  fourierdlem16  40658  fourierdlem17  40659  fourierdlem18  40660  fourierdlem21  40663  fourierdlem22  40664  fourierdlem37  40679  fourierdlem50  40691  fourierdlem51  40692  fourierdlem53  40694  fourierdlem55  40696  fourierdlem57  40698  fourierdlem58  40699  fourierdlem59  40700  fourierdlem60  40701  fourierdlem61  40702  fourierdlem67  40708  fourierdlem68  40709  fourierdlem72  40713  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem78  40719  fourierdlem80  40721  fourierdlem81  40722  fourierdlem83  40724  fourierdlem84  40725  fourierdlem88  40729  fourierdlem92  40733  fourierdlem93  40734  fourierdlem97  40738  fourierdlem101  40742  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  sqwvfoura  40763  elaa2lem  40768  etransclem1  40770  etransclem8  40777  etransclem20  40789  etransclem33  40802  etransclem35  40804  etransclem39  40808  rrxtopnfi  40824  ioorrnopnxrlem  40844  sge0tsms  40915  sge0snmpt  40918  sge0fsummpt  40925  sge0pr  40929  sge0lessmpt  40934  sge0iunmptlemfi  40948  sge0iunmptlemre  40950  sge0iunmpt  40953  sge0rpcpnf  40956  sge0isum  40962  nnfoctbdjlem  40990  psmeasure  41006  voliunsge0lem  41007  meaiuninclem  41015  meaiuninc3v  41019  meaiininclem  41021  omeiunltfirp  41054  carageniuncllem2  41057  caratheodorylem1  41061  caratheodorylem2  41062  isomenndlem  41065  hoicvr  41083  hoicvrrex  41091  ovnsupge0  41092  ovnlecvr  41093  ovnf  41098  ovn0lem  41100  ovnsubaddlem1  41105  ovnsubadd  41107  hsphoif  41111  sge0hsphoire  41124  hoidmv1lelem1  41126  hoidmv1lelem2  41127  hoidmv1lelem3  41128  hoidmv1le  41129  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem5  41134  ovnhoilem1  41136  ovnhoilem2  41137  ovnlecvr2  41145  ovncvr2  41146  hoidifhspf  41153  hspmbllem2  41162  opnvonmbllem2  41168  ovnsubadd2lem  41180  ovolval4lem1  41184  ovolval4lem2  41185  ovolval5lem2  41188  ovnovollem1  41191  ovnovollem2  41192  iccvonmbllem  41213  vonioolem1  41215  vonioolem2  41216  vonicclem1  41218  vonicclem2  41219  smfid  41282  smfmbfcex  41289  smflim  41306  nsssmfmbflem  41307  smfmullem4  41322  smfsuplem1  41338  smfsuplem3  41340  smflimsuplem3  41349  pfxf  41714  fmtnodvds  41781  c0mgm  42234  c0mhm  42235  c0snmgmhm  42239  funcringcsetcALTV2lem3  42363  funcringcsetclem3ALTV  42386  gsumlsscl  42489  ply1mulgsum  42503  lincfsuppcl  42527  linccl  42528  lincvalsc0  42535  lcoc0  42536  linc0scn0  42537  linc1  42539  lincsum  42543  lincscm  42544  lincscmcl  42546  lcoss  42550  lincext1  42568  el0ldep  42580  lincresunit1  42591  lincresunit3  42595  lmod1zr  42607  fdivmptf  42660  refdivmptf  42661  aacllem  42875  amgmwlem  42876  amgmlemALT  42877
  Copyright terms: Public domain W3C validator