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

Theorem fmpttd 6575
Description: Version of fmptd 6574 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 2765 . 2 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
31, 2fmptd 6574 1 (𝜑 → (𝑥𝐴𝐵):𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2155  cmpt 4888  wf 6064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pr 5062
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-fv 6076
This theorem is referenced by:  fmpt3d  6576  fliftrel  6750  off  7110  caofinvl  7122  curry1f  7473  curry2f  7475  pw2f1olem  8271  mapxpen  8333  fsuppmptif  8512  wdom2d  8692  cantnflem1d  8800  cantnflem1  8801  fseqenlem1  9098  ac5num  9110  acni2  9120  infpwfien  9136  fin23lem39  9425  fin1a2lem12  9486  canthp1lem2  9728  wuncval2  9822  gruf  9886  monoord2  13039  seqf1o  13049  ccatcl  13545  swrdcl  13620  pfxf  13669  revcl  13785  revlen  13786  ello1mpt  14539  lo1o12  14551  lo1eq  14586  rlimeq  14587  climmpt2  14591  climrecl  14601  climge0  14602  o1compt  14605  rlimcn1b  14607  rlimdiv  14663  isercoll2  14686  caurcvg2  14695  fsumf1o  14741  sumss  14742  fsumss  14743  fsumcl2lem  14749  fsumadd  14757  isumclim3  14777  isummulc2  14780  fsummulc2  14802  fsumrelem  14825  climfsum  14838  isumshft  14857  divcnv  14871  prodfdiv  14913  fprodf1o  14961  prodss  14962  fprodss  14963  fprodser  14964  fprodcl2lem  14965  fprodmul  14975  fproddiv  14976  fprodn0  14994  iprodclim3  15015  fprodefsum  15109  rpnnen2lem2  15228  iserodd  15821  prmreclem2  15902  1arithlem3  15910  vdwapf  15957  vdwlem4  15969  ramcl  16014  prmodvdslcmf  16032  prdsplusg  16386  prdsmulr  16387  prdsvsca  16388  mrcflem  16534  mreacs  16586  acsfn  16587  homaf  16947  funcestrcsetclem3  17050  funcsetcestrclem3  17064  prfcl  17111  curf1cl  17136  hofcllem  17166  hofcl  17167  yonedalem3a  17182  yonedalem4c  17185  yonedainv  17189  prdspjmhm  17635  pwsco1mhm  17638  pwsco2mhm  17639  gsumz  17642  gsumwspan  17652  vrmdfval  17662  vrmdf  17664  pmtrf  18140  psgnunilem5OLD  18180  odf1o2  18254  sylow2blem1  18301  pj1f  18376  vrgpf  18447  mulgmhm  18499  mulgghm  18500  iscyggen2  18549  cyggenod  18552  iscyg3  18554  gsummptfsadd  18590  gsumzsplit  18593  gsumsplit2  18595  gsumconst  18600  gsummptshft  18602  gsummhm2  18605  gsummptmhm  18606  gsummptfssub  18615  gsummptf1o  18628  gsum2dlem1  18635  gsum2dlem2  18636  gsum2d  18637  prdsgsum  18643  dprdfeq0  18688  dprdlub  18692  dprdz  18696  dprd2dlem1  18707  dprd2da  18708  srglmhm  18802  srgrmhm  18803  ringlghm  18871  ringrghm  18872  gsumdixp  18876  lmodvsghm  19193  lspf  19246  snifpsrbag  19640  psrass1lem  19651  psrmulcllem  19661  psrlidm  19677  psrridm  19678  psrcom  19683  resspsrmul  19691  subrgpsr  19693  mvrf  19698  mplmon  19737  mplmonmul  19738  mplcoe1  19739  mplcoe5lem  19741  mplcoe5  19742  mplbas2  19744  psrbagsn  19768  evlslem4  19781  evlslem2  19785  evlslem6  19786  evlslem3  19787  evlslem1  19788  evlsval2  19793  psropprmul  19881  coe1mul2  19912  coe1tmmul2  19919  coe1tmmul  19920  ply1coe  19939  gsumsmonply1  19946  gsummoncoe1  19947  gsumfsum  20086  regsumfsum  20087  expmhm  20088  expghm  20117  evpmodpmf1o  20215  frlmgsum  20387  frlmsplit2  20388  frlmphl  20396  uvcff  20406  uvcresum  20408  mamulid  20523  mamurid  20524  mdetunilem9  20703  mdetuni0  20704  mdetmul  20706  smadiadetlem3lem1  20750  cpm2mf  20836  m2cpmfo  20840  pmatcollpw1  20860  pmatcollpw3lem  20867  pmatcollpw3fi1lem2  20871  pm2mpcl  20881  mply1topmatcl  20889  mp2pm2mplem2  20891  mp2pm2mp  20895  pm2mpmhmlem2  20903  cayhamlem4  20972  pptbas  21092  tgrest  21243  resttopon  21245  rest0  21253  restfpw  21263  ordtbaslem  21272  ordtuni  21274  ordtrest  21286  cnpfval  21318  pnrmopn  21427  cncmp  21475  discmp  21481  1stcfb  21528  2ndcomap  21541  dis2ndc  21543  comppfsc  21615  kgencmp  21628  ptpjpre1  21654  ptpjcn  21694  ptcldmpt  21697  ptclsg  21698  dfac14  21701  xkoccn  21702  txcnp  21703  ptcnp  21705  uptx  21708  ptcn  21710  ptrescn  21722  xkoptsub  21737  xkoco1cn  21740  xkoco2cn  21741  cnmpt11  21746  pt1hmeo  21889  fbasrn  21967  trfilss  21972  trfg  21974  rnelfmlem  22035  flfcnp2  22090  fclscmpi  22112  alexsublem  22127  ptcmplem3  22137  symgtgp  22184  subgntr  22189  opnsubg  22190  clsnsg  22192  tgpconncomp  22195  eltsms  22215  haustsms  22218  tsmscls  22220  tsms0  22224  tsmsmhm  22228  tgptsmscls  22232  tsmssplit  22234  tsmsxplem1  22235  tsmsxplem2  22236  prdsdsf  22451  prdsxmetlem  22452  imasdsf1olem  22457  prdsbl  22575  stdbdxmet  22599  met1stc  22605  nmf2  22676  xrge0gsumle  22915  xrge0tsms  22916  cncfmpt2ss  22997  cnmptre  23005  evth  23037  evth2  23038  cphnmf  23273  tcphcph  23314  rrxmval  23477  minveclem1  23484  minveclem3b  23488  iunmbl  23611  uniioombllem3  23643  ismbfcn2  23696  mbfeqalem1  23699  mbfeqalem2  23700  mbfss  23704  mbfmulc2re  23706  mbfneg  23708  mbfpos  23709  mbfposr  23710  mbfposb  23711  mbfadd  23719  mbfmulc2  23721  mbfsup  23722  mbfinf  23723  mbflimsup  23724  mbflimlem  23725  mbflim  23726  itg1climres  23772  mbfi1fseqlem3  23775  mbfi1fseqlem4  23776  mbfi1flimlem  23780  mbfi1flim  23781  mbfmullem2  23782  mbfmul  23784  itg2const2  23799  itg2seq  23800  itg2monolem1  23808  itg2monolem2  23809  itg2monolem3  23810  itg2mono  23811  itg2gt0  23818  itg2cnlem1  23819  itg2cnlem2  23820  itg2cn  23821  iblss  23862  itgitg1  23866  itgle  23867  itgeqa  23871  itgss3  23872  ibladdlem  23877  itgaddlem1  23880  iblabslem  23885  iblabs  23886  iblabsr  23887  iblmulc2  23888  itgmulc2lem1  23889  bddmulibl  23896  itggt0  23899  itgcn  23900  ellimc2  23932  limcmpt  23938  limcres  23941  limccnp  23946  limccnp2  23947  limcco  23948  perfdvf  23958  dvcnp2  23974  dvaddbr  23992  dvmulbr  23993  dvcjbr  24003  dvexp  24007  dvrec  24009  dvmptres3  24010  dvmptadd  24014  dvmptmul  24015  dvmptres2  24016  dvmptcmul  24018  dvmptcj  24022  dvmptntr  24025  dvmptco  24026  dvcnvlem  24030  dvef  24034  dvferm1  24039  dvferm2  24041  rolle  24044  dvlipcn  24048  dvle  24061  dvivth  24064  lhop1lem  24067  lhop1  24068  lhop2  24069  lhop  24070  dvfsumle  24075  dvfsumge  24076  dvmptrecl  24078  dvfsumlem2  24081  itgsubstlem  24102  tdeglem4  24111  coe1mul3  24150  elply2  24243  plyf  24245  elplyd  24249  plypf1  24259  coeeq2  24289  coemullem  24297  coe1termlem  24305  dvply2g  24331  elqaalem2  24366  taylfvallem  24403  taylf  24406  tayl0  24407  taylpfval  24410  taylpf  24411  taylthlem1  24418  taylthlem2  24419  ulmshftlem  24434  ulmshft  24435  ulmcau  24440  ulmss  24442  ulmdvlem1  24445  ulmdvlem3  24447  mtest  24449  mtestbdd  24450  itgulm2  24454  psergf  24457  dvradcnv  24466  pserulm  24467  pserdvlem2  24473  abelthlem9  24485  pige3  24561  logtayl  24697  logccv  24700  loglesqrt  24790  logbf  24818  leibpi  24960  rlimcnp  24983  rlimcnp2  24984  xrlimcnp  24986  efrlim  24987  dfef2  24988  o1cxp  24992  cxp2lim  24994  amgmlem  25007  lgamgulmlem2  25047  lgamgulmlem6  25051  lgamcvg2  25072  regamcl  25078  relgamcl  25079  basellem2  25099  sqff1o  25199  fsumvma  25229  dchrelbasd  25255  lgseisenlem3  25393  lgseisenlem4  25394  chpo1ub  25460  dchrisum0lem2a  25497  logsqvma2  25523  pnt2  25593  pnt  25594  lmif  25968  incistruhgr  26251  vtxdgf  26658  minvecolem1  28121  hoaddcl  29008  homulcl  29009  brafn  29197  kbop  29203  off2  29828  fpwrelmap  29892  gsummpt2d  30163  gsumvsca1  30164  gsumvsca2  30165  xrge0tsmsd  30167  ordtrestNEW  30349  esumf1o  30494  esumadd  30501  esumcst  30507  esumpfinval  30519  esumpcvgval  30522  esumcvg  30530  esumsup  30533  measinb  30666  measdivcst  30670  sitgclg  30786  dstfrvclim1  30922  gsumncl  30997  gsumnunsn  30998  fdvneggt  31061  fdvnegge  31063  itgexpif  31067  logdivsqrle  31111  indispconn  31596  cvxpconn  31604  cvmsss2  31636  cvmliftlem6  31652  cvmliftlem8  31654  mrsubcv  31787  mrsubff  31789  mrsubrn  31790  mrsubccat  31795  elmrsubrn  31797  msubrn  31806  msubff  31807  divcnvlin  31995  faclimlem2  32007  faclim  32009  faclim2  32011  knoppcnlem5  32858  knoppcnlem8  32861  knoppcnlem10  32863  knoppcnlem11  32864  curf  33743  finixpnum  33750  matunitlindflem1  33761  matunitlindflem2  33762  ptrest  33764  poimirlem17  33782  poimirlem20  33785  poimirlem24  33789  poimirlem30  33795  broucube  33799  mblfinlem2  33803  volsupnfl  33810  mbfposadd  33812  itg2addnclem2  33817  itg2gt0cn  33820  ibladdnclem  33821  itgaddnclem1  33823  itgaddnc  33825  iblabsnclem  33828  iblabsnc  33829  iblmulc2nc  33830  itgmulc2nclem1  33831  itgmulc2nclem2  33832  itgmulc2nc  33833  itgabsnc  33834  bddiblnc  33835  itggt0cn  33837  ftc1cnnc  33839  ftc1anclem1  33840  ftc1anclem2  33841  ftc1anclem3  33842  ftc1anclem4  33843  ftc1anclem5  33844  ftc1anclem6  33845  ftc1anclem7  33846  ftc1anclem8  33847  ftc1anc  33848  areacirclem4  33858  upixp  33879  totbndbnd  33942  prdsbnd  33946  cntotbnd  33949  rrnequiv  33988  lsatlss  34884  tendoplcl  36669  tendoicl  36684  cmpfiiin  37870  mzpclall  37900  mzpindd  37919  fphpdo  37991  dnnumch3  38226  kelac1  38242  dfac21  38245  itgpowd  38408  rfovcnvf1od  38904  fsovfd  38912  fsovcnvlem  38913  clsk3nimkb  38944  expgrowth  39140  mptelpm  39936  mapss2  39974  monoord2xrv  40283  expcnfg  40393  clim1fr1  40403  sumnnodd  40432  limsupvaluz2  40540  supcnvlimsup  40542  climliminflimsupd  40603  liminfltlem  40606  cncfmptssg  40653  cncfcompt  40666  cxpcncf2  40683  dvsinax  40697  fperdvper  40703  dvcosax  40711  dvnmptdivc  40723  dvnprodlem2  40732  dvnprodlem3  40733  iblsplit  40751  itgcoscmulx  40754  itgiccshift  40765  itgperiod  40766  itgsbtaddcnst  40767  dirkerf  40883  dirkeritg  40888  hoidmvlelem1  41381  hoidmvlelem5  41385  ovnhoilem1  41387  ovnhoilem2  41388  ovnlecvr2  41396  ovncvr2  41397  hoidifhspf  41404  hspmbllem2  41413  opnvonmbllem2  41419  iccvonmbllem  41464  vonioolem1  41466  vonioolem2  41467  vonicclem1  41469  vonicclem2  41470  smfid  41533  funcringcsetcALTV2lem3  42639  funcringcsetclem3ALTV  42662  gsumlsscl  42765  ply1mulgsum  42779  lincfsuppcl  42803  linccl  42804  lincsum  42819  lincscmcl  42822  lcoss  42826  lincext1  42844  el0ldep  42856  lincresunit1  42867  lincresunit3  42871  lmod1zr  42883  fdivmptf  42936  refdivmptf  42937  aacllem  43151  amgmwlem  43152
  Copyright terms: Public domain W3C validator