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

Theorem fmpttd 7064
Description: Version of fmptd 7063 with inlined definition. Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Proof shortened by BJ, 16-Aug-2022.)
Hypothesis
Ref Expression
fmpttd.1 ((𝜑𝑥𝐴) → 𝐵𝐶)
Assertion
Ref Expression
fmpttd (𝜑 → (𝑥𝐴𝐵):𝐴𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜑,𝑥
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem fmpttd
StepHypRef Expression
1 fmpttd.1 . 2 ((𝜑𝑥𝐴) → 𝐵𝐶)
2 eqid 2737 . 2 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
31, 2fmptd 7063 1 (𝜑 → (𝑥𝐴𝐵):𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  cmpt 5189  wf 6493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-fun 6499  df-fn 6500  df-f 6501
This theorem is referenced by:  fmpt3d  7065  fliftrel  7254  pw2f1olem  9021  mapxpen  9088  fsuppmptif  9336  wdom2d  9517  cantnflem1d  9625  cantnflem1  9626  ac5num  9973  acni2  9983  infpwfien  9999  fin23lem39  10287  fin1a2lem12  10348  canthp1lem2  10590  wuncval2  10684  gruf  10748  monoord2  13940  seqf1o  13950  ccatcl  14463  swrdcl  14534  swrdwrdsymb  14551  revcl  14650  revlen  14651  ello1mpt  15404  lo1o12  15416  lo1eq  15451  rlimeq  15452  climmpt2  15456  climrecl  15466  climge0  15467  o1compt  15470  rlimcn1b  15472  rlimdiv  15531  isercoll2  15554  caurcvg2  15563  fsumf1o  15609  sumss  15610  fsumss  15611  fsumcl2lem  15617  fsumadd  15626  isumclim3  15645  isummulc2  15648  fsummulc2  15670  fsumrelem  15693  climfsum  15706  isumshft  15725  divcnv  15739  prodfdiv  15782  fprodf1o  15830  prodss  15831  fprodss  15832  fprodser  15833  fprodcl2lem  15834  fprodmul  15844  fproddiv  15845  fprodn0  15863  iprodclim3  15884  fprodefsum  15978  iserodd  16708  prmreclem2  16790  vdwapf  16845  vdwlem4  16857  ramcl  16902  prmodvdslcmf  16920  prdsplusg  17341  prdsmulr  17342  prdsvsca  17343  mrcflem  17487  mreacs  17539  acsfn  17540  hofcllem  18148  hofcl  18149  yonedalem3a  18164  yonedalem4c  18167  yonedainv  18171  prdspjmhm  18640  pwsco1mhm  18643  pwsco2mhm  18644  gsumz  18647  gsumwspan  18657  odf1o1  19355  odf1o2  19356  sylow2blem1  19403  mulgmhm  19607  mulgghm  19608  iscyggen2  19659  cyggenod  19662  iscyg3  19664  gsumzsplit  19705  gsumsplit2  19707  gsumconst  19712  gsummptshft  19714  gsummhm2  19717  gsummptmhm  19718  gsummptf1o  19741  gsum2dlem1  19748  gsum2dlem2  19749  gsum2d  19750  prdsgsum  19759  dprdfeq0  19802  dprdlub  19806  dprdz  19810  dprd2dlem1  19821  dprd2da  19822  srglmhm  19953  srgrmhm  19954  ringlghm  20029  ringrghm  20030  gsumdixp  20034  pwspjmhmmgpd  20044  lmodvsghm  20386  gsumfsum  20867  regsumfsum  20868  expmhm  20869  expghm  20899  evpmodpmf1o  21003  frlmgsum  21181  frlmsplit2  21182  frlmphl  21190  uvcff  21200  uvcresum  21202  snifpsrbag  21327  psrass1lemOLD  21345  psrass1lem  21348  psrmulcllem  21358  psrlidm  21375  psrridm  21376  psrcom  21381  resspsrmul  21389  mvrf  21396  mplmon  21439  mplmonmul  21440  mplcoe1  21441  mplcoe5lem  21443  mplcoe5  21444  mplbas2  21446  psrbagsn  21474  evlslem4  21487  evlslem2  21492  evlslem3  21493  evlslem6  21494  evlslem1  21495  evlsval2  21500  psropprmul  21612  coe1mul2  21643  coe1tmmul2  21650  coe1tmmul  21651  ply1coe  21670  gsumsmonply1  21677  gsummoncoe1  21678  mamulid  21793  mamurid  21794  mdetunilem9  21972  mdetuni0  21973  mdetmul  21975  smadiadetlem3lem1  22018  m2cpmfo  22108  pmatcollpw1  22128  pmatcollpw3lem  22135  pmatcollpw3fi1lem2  22139  pm2mpcl  22149  mply1topmatcl  22157  mp2pm2mplem2  22159  mp2pm2mp  22163  pm2mpmhmlem2  22171  cayhamlem4  22240  pptbas  22361  tgrest  22513  resttopon  22515  rest0  22523  restfpw  22533  ordtbaslem  22542  ordtuni  22544  ordtrest  22556  cnpfval  22588  pnrmopn  22697  cncmp  22746  discmp  22752  1stcfb  22799  2ndcomap  22812  dis2ndc  22814  comppfsc  22886  kgencmp  22899  ptpjpre1  22925  ptpjcn  22965  ptcldmpt  22968  ptclsg  22969  dfac14  22972  xkoccn  22973  txcnp  22974  ptcnp  22976  uptx  22979  ptcn  22981  ptrescn  22993  xkoptsub  23008  xkoco1cn  23011  xkoco2cn  23012  cnmpt11  23017  pt1hmeo  23160  fbasrn  23238  trfilss  23243  trfg  23245  rnelfmlem  23306  flfcnp2  23361  fclscmpi  23383  alexsublem  23398  ptcmplem3  23408  symgtgp  23460  subgntr  23461  opnsubg  23462  clsnsg  23464  tgpconncomp  23467  eltsms  23487  haustsms  23490  tsmscls  23492  tsms0  23496  tsmsmhm  23500  tgptsmscls  23504  tsmssplit  23506  tsmsxplem1  23507  tsmsxplem2  23508  prdsdsf  23723  prdsxmetlem  23724  imasdsf1olem  23729  prdsbl  23850  stdbdxmet  23874  met1stc  23880  xrge0gsumle  24199  xrge0tsms  24200  cncfmpt2ss  24282  cnmptre  24293  evth  24325  evth2  24326  tcphcph  24604  rrxmval  24772  minveclem1  24791  minveclem3b  24795  iunmbl  24920  uniioombllem3  24952  ismbfcn2  25005  mbfeqalem1  25008  mbfeqalem2  25009  mbfss  25013  mbfmulc2re  25015  mbfneg  25017  mbfpos  25018  mbfposr  25019  mbfposb  25020  mbfadd  25028  mbfmulc2  25030  mbfsup  25031  mbfinf  25032  mbflimsup  25033  mbflimlem  25034  mbflim  25035  itg1climres  25082  mbfi1fseqlem3  25085  mbfi1fseqlem4  25086  mbfi1flimlem  25090  mbfi1flim  25091  mbfmullem2  25092  mbfmul  25094  itg2const2  25109  itg2seq  25110  itg2monolem1  25118  itg2monolem2  25119  itg2monolem3  25120  itg2mono  25121  itg2gt0  25128  itg2cnlem1  25129  itg2cnlem2  25130  itg2cn  25131  iblss  25172  itgitg1  25176  itgle  25177  itgeqa  25181  itgss3  25182  ibladdlem  25187  itgaddlem1  25190  iblabslem  25195  iblabs  25196  iblabsr  25197  iblmulc2  25198  itgmulc2lem1  25199  bddmulibl  25206  bddiblnc  25209  itggt0  25211  itgcn  25212  ellimc2  25244  limcmpt  25250  limcres  25253  limccnp  25258  limccnp2  25259  limcco  25260  perfdvf  25270  dvcnp2  25287  dvaddbr  25305  dvmulbr  25306  dvcjbr  25316  dvexp  25320  dvrec  25322  dvmptres3  25323  dvmptadd  25327  dvmptmul  25328  dvmptres2  25329  dvmptcmul  25331  dvmptcj  25335  dvmptntr  25338  dvmptco  25339  dvcnvlem  25343  dvef  25347  dvferm1  25352  dvferm2  25354  rolle  25357  dvlipcn  25361  dvle  25374  dvivth  25377  lhop1lem  25380  lhop1  25381  lhop2  25382  lhop  25383  dvfsumle  25388  dvfsumge  25389  dvmptrecl  25391  dvfsumlem2  25394  itgsubstlem  25415  itgpowd  25417  tdeglem4  25427  tdeglem4OLD  25428  coe1mul3  25467  elply2  25560  plyf  25562  elplyd  25566  plypf1  25576  coeeq2  25606  coemullem  25614  coe1termlem  25622  dvply2g  25648  elqaalem2  25683  taylfvallem  25720  taylf  25723  tayl0  25724  taylpfval  25727  taylthlem1  25735  taylthlem2  25736  ulmcau  25757  ulmss  25759  ulmdvlem3  25764  mtest  25766  mtestbdd  25767  itgulm2  25771  dvradcnv  25783  pserulm  25784  pserdvlem2  25790  abelthlem9  25802  pige3ALT  25879  logtayl  26018  logccv  26021  loglesqrt  26114  leibpi  26295  rlimcnp  26318  rlimcnp2  26319  xrlimcnp  26321  efrlim  26322  dfef2  26323  o1cxp  26327  cxp2lim  26329  amgmlem  26342  lgamgulmlem2  26382  lgamgulmlem6  26386  lgamcvg2  26407  regamcl  26413  relgamcl  26414  basellem2  26434  basellem3  26435  sqff1o  26534  fsumvma  26564  dchrelbasd  26590  lgseisenlem3  26728  lgseisenlem4  26729  chpo1ub  26831  dchrisum0lem2a  26868  logsqvma2  26894  pnt2  26964  pnt  26965  incistruhgr  28033  minvecolem1  29819  hoaddcl  30703  homulcl  30704  cofmpt2  31551  fpwrelmap  31653  gsummpt2d  31894  xrge0tsmsd  31902  gsumvsca1  32064  gsumvsca2  32065  elrspunidl  32206  fedgmullem1  32327  fedgmullem2  32328  ordtrestNEW  32505  esumf1o  32652  esumadd  32659  esumcst  32665  esumpfinval  32677  esumpcvgval  32680  esumcvg  32688  esumsup  32691  measinb  32823  measdivcst  32826  sitgclg  32945  dstfrvclim1  33080  gsumncl  33155  gsumnunsn  33156  fdvneggt  33216  fdvnegge  33218  itgexpif  33222  logdivsqrle  33266  indispconn  33831  cvxpconn  33839  cvmsss2  33871  cvmliftlem6  33887  cvmliftlem8  33889  mrsubcv  34107  mrsubff  34109  mrsubrn  34110  mrsubccat  34115  elmrsubrn  34117  msubrn  34126  msubff  34127  divcnvlin  34308  faclimlem2  34320  faclim  34322  faclim2  34324  knoppcnlem5  34963  knoppcnlem8  34966  knoppcnlem10  34968  knoppcnlem11  34969  curf  36059  finixpnum  36066  matunitlindflem1  36077  matunitlindflem2  36078  ptrest  36080  poimirlem17  36098  poimirlem20  36101  poimirlem24  36105  poimirlem30  36111  broucube  36115  mblfinlem2  36119  volsupnfl  36126  mbfposadd  36128  itg2addnclem2  36133  itg2gt0cn  36136  ibladdnclem  36137  itgaddnclem1  36139  itgaddnc  36141  iblabsnclem  36144  iblabsnc  36145  iblmulc2nc  36146  itgmulc2nclem1  36147  itgmulc2nclem2  36148  itgmulc2nc  36149  itgabsnc  36150  itggt0cn  36151  ftc1cnnc  36153  ftc1anclem1  36154  ftc1anclem2  36155  ftc1anclem3  36156  ftc1anclem4  36157  ftc1anclem5  36158  ftc1anclem6  36159  ftc1anclem7  36160  ftc1anclem8  36161  ftc1anc  36162  areacirclem4  36172  upixp  36191  totbndbnd  36251  prdsbnd  36255  cntotbnd  36258  rrnequiv  36297  lsatlss  37461  tendoplcl  39247  tendoicl  39262  aks4d1p1p5  40535  aks4d1p9  40548  sticksstones10  40566  sticksstones17  40574  sticksstones18  40575  pwsgprod  40735  rhmmpllem1  40740  rhmmpllem2  40741  evlsval3  40747  evlsbagval  40751  fsuppind  40768  fsuppssind  40771  mhpind  40772  mhphflem  40773  mhphf  40774  cmpfiiin  41023  mzpclall  41053  mzpindd  41072  fphpdo  41143  dnnumch3  41377  kelac1  41393  dfac21  41396  cantnfresb  41661  cantnf2  41662  rfovcnvf1od  42283  fsovfd  42291  fsovcnvlem  42292  clsk3nimkb  42319  mnringmulrcld  42515  expgrowth  42622  mptelpm  43400  mapss2  43433  monoord2xrv  43726  expcnfg  43839  clim1fr1  43849  sumnnodd  43878  limsupvaluz2  43986  supcnvlimsup  43988  climliminflimsupd  44049  liminfltlem  44052  cncfmptssg  44119  cncfcompt  44131  cxpcncf2  44147  dvsinax  44161  fperdvper  44167  dvcosax  44174  dvnmptdivc  44186  dvnprodlem2  44195  dvnprodlem3  44196  iblsplit  44214  itgcoscmulx  44217  itgiccshift  44228  itgperiod  44229  itgsbtaddcnst  44230  dirkerf  44345  dirkeritg  44350  hoidmvlelem1  44843  hoidmvlelem5  44847  ovnhoilem1  44849  ovnhoilem2  44850  ovnlecvr2  44858  ovncvr2  44859  hoidifhspf  44866  hspmbllem2  44875  opnvonmbllem2  44881  iccvonmbllem  44926  vonioolem1  44928  vonioolem2  44929  vonicclem1  44931  vonicclem2  44932  smfid  45000  cfsetsnfsetf  45299  funcringcsetcALTV2lem3  46343  funcringcsetclem3ALTV  46366  gsumlsscl  46466  ply1mulgsum  46478  lincfsuppcl  46501  linccl  46502  lincsum  46517  lincscmcl  46520  lcoss  46524  lincext1  46542  el0ldep  46554  lincresunit1  46565  lincresunit3  46569  lmod1zr  46581  fdivmptf  46634  refdivmptf  46635  1arymaptf  46734  aacllem  47255  amgmwlem  47256
  Copyright terms: Public domain W3C validator