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

Theorem fmpttd 6872
Description: Version of fmptd 6871 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 2821 . 2 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
31, 2fmptd 6871 1 (𝜑 → (𝑥𝐴𝐵):𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  cmpt 5138  wf 6345
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-fv 6357
This theorem is referenced by:  fmpt3d  6873  fliftrel  7050  pw2f1olem  8610  mapxpen  8672  fsuppmptif  8852  wdom2d  9033  cantnflem1d  9140  cantnflem1  9141  ac5num  9451  acni2  9461  infpwfien  9477  fin23lem39  9761  fin1a2lem12  9822  canthp1lem2  10064  wuncval2  10158  gruf  10222  monoord2  13391  seqf1o  13401  ccatcl  13916  swrdcl  13997  swrdwrdsymb  14014  revcl  14113  revlen  14114  ello1mpt  14868  lo1o12  14880  lo1eq  14915  rlimeq  14916  climmpt2  14920  climrecl  14930  climge0  14931  o1compt  14934  rlimcn1b  14936  rlimdiv  14992  isercoll2  15015  caurcvg2  15024  fsumf1o  15070  sumss  15071  fsumss  15072  fsumcl2lem  15078  fsumadd  15086  isumclim3  15104  isummulc2  15107  fsummulc2  15129  fsumrelem  15152  climfsum  15165  isumshft  15184  divcnv  15198  prodfdiv  15242  fprodf1o  15290  prodss  15291  fprodss  15292  fprodser  15293  fprodcl2lem  15294  fprodmul  15304  fproddiv  15305  fprodn0  15323  iprodclim3  15344  fprodefsum  15438  iserodd  16162  prmreclem2  16243  vdwapf  16298  vdwlem4  16310  ramcl  16355  prmodvdslcmf  16373  prdsplusg  16721  prdsmulr  16722  prdsvsca  16723  mrcflem  16867  mreacs  16919  acsfn  16920  hofcllem  17498  hofcl  17499  yonedalem3a  17514  yonedalem4c  17517  yonedainv  17521  prdspjmhm  17983  pwsco1mhm  17986  pwsco2mhm  17987  gsumz  17990  gsumwspan  18001  odf1o1  18628  odf1o2  18629  sylow2blem1  18676  mulgmhm  18879  mulgghm  18880  iscyggen2  18931  cyggenod  18934  iscyg3  18936  gsumzsplit  18978  gsumsplit2  18980  gsumconst  18985  gsummptshft  18987  gsummhm2  18990  gsummptmhm  18991  gsummptf1o  19014  gsum2dlem1  19021  gsum2dlem2  19022  gsum2d  19023  prdsgsum  19032  dprdfeq0  19075  dprdlub  19079  dprdz  19083  dprd2dlem1  19094  dprd2da  19095  srglmhm  19216  srgrmhm  19217  ringlghm  19285  ringrghm  19286  gsumdixp  19290  lmodvsghm  19626  snifpsrbag  20076  psrass1lem  20087  psrmulcllem  20097  psrlidm  20113  psrridm  20114  psrcom  20119  resspsrmul  20127  mvrf  20134  mplmon  20174  mplmonmul  20175  mplcoe1  20176  mplcoe5lem  20178  mplcoe5  20179  mplbas2  20181  psrbagsn  20205  evlslem4  20218  evlslem2  20222  evlslem3  20223  evlslem6  20224  evlslem1  20225  evlsval2  20230  psropprmul  20336  coe1mul2  20367  coe1tmmul2  20374  coe1tmmul  20375  ply1coe  20394  gsumsmonply1  20401  gsummoncoe1  20402  gsumfsum  20542  regsumfsum  20543  expmhm  20544  expghm  20573  evpmodpmf1o  20670  frlmgsum  20846  frlmsplit2  20847  frlmphl  20855  uvcff  20865  uvcresum  20867  mamulid  20980  mamurid  20981  mdetunilem9  21159  mdetuni0  21160  mdetmul  21162  smadiadetlem3lem1  21205  m2cpmfo  21294  pmatcollpw1  21314  pmatcollpw3lem  21321  pmatcollpw3fi1lem2  21325  pm2mpcl  21335  mply1topmatcl  21343  mp2pm2mplem2  21345  mp2pm2mp  21349  pm2mpmhmlem2  21357  cayhamlem4  21426  pptbas  21546  tgrest  21697  resttopon  21699  rest0  21707  restfpw  21717  ordtbaslem  21726  ordtuni  21728  ordtrest  21740  cnpfval  21772  pnrmopn  21881  cncmp  21930  discmp  21936  1stcfb  21983  2ndcomap  21996  dis2ndc  21998  comppfsc  22070  kgencmp  22083  ptpjpre1  22109  ptpjcn  22149  ptcldmpt  22152  ptclsg  22153  dfac14  22156  xkoccn  22157  txcnp  22158  ptcnp  22160  uptx  22163  ptcn  22165  ptrescn  22177  xkoptsub  22192  xkoco1cn  22195  xkoco2cn  22196  cnmpt11  22201  pt1hmeo  22344  fbasrn  22422  trfilss  22427  trfg  22429  rnelfmlem  22490  flfcnp2  22545  fclscmpi  22567  alexsublem  22582  ptcmplem3  22592  symgtgp  22639  subgntr  22644  opnsubg  22645  clsnsg  22647  tgpconncomp  22650  eltsms  22670  haustsms  22673  tsmscls  22675  tsms0  22679  tsmsmhm  22683  tgptsmscls  22687  tsmssplit  22689  tsmsxplem1  22690  tsmsxplem2  22691  prdsdsf  22906  prdsxmetlem  22907  imasdsf1olem  22912  prdsbl  23030  stdbdxmet  23054  met1stc  23060  xrge0gsumle  23370  xrge0tsms  23371  cncfmpt2ss  23452  cnmptre  23460  evth  23492  evth2  23493  tcphcph  23769  rrxmval  23937  minveclem1  23956  minveclem3b  23960  iunmbl  24083  uniioombllem3  24115  ismbfcn2  24168  mbfeqalem1  24171  mbfeqalem2  24172  mbfss  24176  mbfmulc2re  24178  mbfneg  24180  mbfpos  24181  mbfposr  24182  mbfposb  24183  mbfadd  24191  mbfmulc2  24193  mbfsup  24194  mbfinf  24195  mbflimsup  24196  mbflimlem  24197  mbflim  24198  itg1climres  24244  mbfi1fseqlem3  24247  mbfi1fseqlem4  24248  mbfi1flimlem  24252  mbfi1flim  24253  mbfmullem2  24254  mbfmul  24256  itg2const2  24271  itg2seq  24272  itg2monolem1  24280  itg2monolem2  24281  itg2monolem3  24282  itg2mono  24283  itg2gt0  24290  itg2cnlem1  24291  itg2cnlem2  24292  itg2cn  24293  iblss  24334  itgitg1  24338  itgle  24339  itgeqa  24343  itgss3  24344  ibladdlem  24349  itgaddlem1  24352  iblabslem  24357  iblabs  24358  iblabsr  24359  iblmulc2  24360  itgmulc2lem1  24361  bddmulibl  24368  itggt0  24371  itgcn  24372  ellimc2  24404  limcmpt  24410  limcres  24413  limccnp  24418  limccnp2  24419  limcco  24420  perfdvf  24430  dvcnp2  24446  dvaddbr  24464  dvmulbr  24465  dvcjbr  24475  dvexp  24479  dvrec  24481  dvmptres3  24482  dvmptadd  24486  dvmptmul  24487  dvmptres2  24488  dvmptcmul  24490  dvmptcj  24494  dvmptntr  24497  dvmptco  24498  dvcnvlem  24502  dvef  24506  dvferm1  24511  dvferm2  24513  rolle  24516  dvlipcn  24520  dvle  24533  dvivth  24536  lhop1lem  24539  lhop1  24540  lhop2  24541  lhop  24542  dvfsumle  24547  dvfsumge  24548  dvmptrecl  24550  dvfsumlem2  24553  itgsubstlem  24574  tdeglem4  24583  coe1mul3  24622  elply2  24715  plyf  24717  elplyd  24721  plypf1  24731  coeeq2  24761  coemullem  24769  coe1termlem  24777  dvply2g  24803  elqaalem2  24838  taylfvallem  24875  taylf  24878  tayl0  24879  taylpfval  24882  taylthlem1  24890  taylthlem2  24891  ulmcau  24912  ulmss  24914  ulmdvlem3  24919  mtest  24921  mtestbdd  24922  itgulm2  24926  dvradcnv  24938  pserulm  24939  pserdvlem2  24945  abelthlem9  24957  pige3ALT  25034  logtayl  25170  logccv  25173  loglesqrt  25266  leibpi  25448  rlimcnp  25471  rlimcnp2  25472  xrlimcnp  25474  efrlim  25475  dfef2  25476  o1cxp  25480  cxp2lim  25482  amgmlem  25495  lgamgulmlem2  25535  lgamgulmlem6  25539  lgamcvg2  25560  regamcl  25566  relgamcl  25567  basellem2  25587  basellem3  25588  sqff1o  25687  fsumvma  25717  dchrelbasd  25743  lgseisenlem3  25881  lgseisenlem4  25882  chpo1ub  25984  dchrisum0lem2a  26021  logsqvma2  26047  pnt2  26117  pnt  26118  incistruhgr  26792  minvecolem1  28579  hoaddcl  29463  homulcl  29464  cofmpt2  30308  fpwrelmap  30396  gsummpt2d  30615  xrge0tsmsd  30620  gsumvsca1  30782  gsumvsca2  30783  fedgmullem1  30925  fedgmullem2  30926  ordtrestNEW  31064  esumf1o  31209  esumadd  31216  esumcst  31222  esumpfinval  31234  esumpcvgval  31237  esumcvg  31245  esumsup  31248  measinb  31380  measdivcst  31383  sitgclg  31500  dstfrvclim1  31635  gsumncl  31710  gsumnunsn  31711  fdvneggt  31771  fdvnegge  31773  itgexpif  31777  logdivsqrle  31821  indispconn  32379  cvxpconn  32387  cvmsss2  32419  cvmliftlem6  32435  cvmliftlem8  32437  mrsubcv  32655  mrsubff  32657  mrsubrn  32658  mrsubccat  32663  elmrsubrn  32665  msubrn  32674  msubff  32675  divcnvlin  32862  faclimlem2  32874  faclim  32876  faclim2  32878  knoppcnlem5  33734  knoppcnlem8  33737  knoppcnlem10  33739  knoppcnlem11  33740  curf  34752  finixpnum  34759  matunitlindflem1  34770  matunitlindflem2  34771  ptrest  34773  poimirlem17  34791  poimirlem20  34794  poimirlem24  34798  poimirlem30  34804  broucube  34808  mblfinlem2  34812  volsupnfl  34819  mbfposadd  34821  itg2addnclem2  34826  itg2gt0cn  34829  ibladdnclem  34830  itgaddnclem1  34832  itgaddnc  34834  iblabsnclem  34837  iblabsnc  34838  iblmulc2nc  34839  itgmulc2nclem1  34840  itgmulc2nclem2  34841  itgmulc2nc  34842  itgabsnc  34843  bddiblnc  34844  itggt0cn  34846  ftc1cnnc  34848  ftc1anclem1  34849  ftc1anclem2  34850  ftc1anclem3  34851  ftc1anclem4  34852  ftc1anclem5  34853  ftc1anclem6  34854  ftc1anclem7  34855  ftc1anclem8  34856  ftc1anc  34857  areacirclem4  34867  upixp  34887  totbndbnd  34950  prdsbnd  34954  cntotbnd  34957  rrnequiv  34996  lsatlss  36014  tendoplcl  37799  tendoicl  37814  cmpfiiin  39174  mzpclall  39204  mzpindd  39223  fphpdo  39294  dnnumch3  39527  kelac1  39543  dfac21  39546  itgpowd  39701  rfovcnvf1od  40230  fsovfd  40238  fsovcnvlem  40239  clsk3nimkb  40270  expgrowth  40547  mptelpm  41312  mapss2  41348  monoord2xrv  41640  expcnfg  41752  clim1fr1  41762  sumnnodd  41791  limsupvaluz2  41899  supcnvlimsup  41901  climliminflimsupd  41962  liminfltlem  41965  cncfmptssg  42033  cncfcompt  42046  cxpcncf2  42063  dvsinax  42077  fperdvper  42083  dvcosax  42091  dvnmptdivc  42103  dvnprodlem2  42112  dvnprodlem3  42113  iblsplit  42131  itgcoscmulx  42134  itgiccshift  42145  itgperiod  42146  itgsbtaddcnst  42147  dirkerf  42263  dirkeritg  42268  hoidmvlelem1  42758  hoidmvlelem5  42762  ovnhoilem1  42764  ovnhoilem2  42765  ovnlecvr2  42773  ovncvr2  42774  hoidifhspf  42781  hspmbllem2  42790  opnvonmbllem2  42796  iccvonmbllem  42841  vonioolem1  42843  vonioolem2  42844  vonicclem1  42846  vonicclem2  42847  smfid  42910  funcringcsetcALTV2lem3  44207  funcringcsetclem3ALTV  44230  gsumlsscl  44329  ply1mulgsum  44342  lincfsuppcl  44366  linccl  44367  lincsum  44382  lincscmcl  44385  lcoss  44389  lincext1  44407  el0ldep  44419  lincresunit1  44430  lincresunit3  44434  lmod1zr  44446  fdivmptf  44499  refdivmptf  44500  aacllem  44800  amgmwlem  44801
  Copyright terms: Public domain W3C validator