Theorem fmpttd 7085

Description: Version of fmptd 7084 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

Step	Hyp	Ref	Expression
1		fmpttd.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
2		eqid 2756	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	1, 2	fmptd 7084	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2136   ↦ cmpt 5175  ⟶wf 6506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728  ax-sep 5240  ax-pr 5384

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-br 5095  df-opab 5157  df-mpt 5176  df-id 5535  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-fun 6512  df-fn 6513  df-f 6514

This theorem is referenced by:  fmpt3d  7086  fliftrel  7281  fsetfocdm  8831  pw2f1olem  9042  mapxpen  9104  fsuppssov1  9320  fsuppmptif  9335  wdom2d  9518  cantnflem1d  9633  cantnflem1  9634  ac5num  9982  acni2  9992  infpwfien  10008  fin23lem39  10297  fin1a2lem12  10358  canthp1lem2  10601  wuncval2  10695  gruf  10759  monoord2  14036  seqf1o  14046  ccatcl  14577  swrdcl  14649  swrdwrdsymb  14666  revcl  14764  revlen  14765  ello1mpt  15524  lo1o12  15536  lo1eq  15571  rlimeq  15572  climmpt2  15576  climrecl  15586  climge0  15587  o1compt  15590  rlimcn1b  15592  rlimdiv  15649  isercoll2  15672  caurcvg2  15681  fsumf1o  15726  sumss  15727  fsumss  15728  fsumcl2lem  15734  fsumadd  15743  isumclim3  15762  isummulc2  15765  fsummulc2  15787  fsumrelem  15811  climfsum  15824  isumshft  15845  divcnv  15859  prodfdiv  15902  fprodf1o  15952  prodss  15953  fprodss  15954  fprodser  15955  fprodcl2lem  15956  fprodmul  15966  fproddiv  15967  fprodn0  15985  iprodclim3  16006  fprodefsum  16101  iserodd  16847  prmreclem2  16929  vdwapf  16984  vdwlem4  16996  ramcl  17041  prmodvdslcmf  17059  prdsplusg  17463  prdsmulr  17464  prdsvsca  17465  mrcflem  17614  mreacs  17666  acsfn  17667  hofcllem  18266  hofcl  18267  yonedalem3a  18282  yonedalem4c  18285  yonedainv  18289  prdspjmhm  18839  pwsco1mhm  18842  pwsco2mhm  18843  gsumz  18846  gsumwspan  18856  smndex1gbas  18912  odf1o1  19588  odf1o2  19589  sylow2blem1  19636  mulgmhm  19843  mulgghm  19844  iscyggen2  19897  cyggenod  19900  iscyg3  19902  gsumzsplit  19943  gsumsplit2  19945  gsumconst  19950  gsummptshft  19952  gsummhm2  19955  gsummptmhm  19956  gsummptf1o  19979  gsum2dlem1  19986  gsum2dlem2  19987  gsum2d  19988  prdsgsum  19997  dprdfeq0  20040  dprdlub  20044  dprdz  20048  dprd2dlem1  20059  dprd2da  20060  srglmhm  20243  srgrmhm  20244  ringlghm  20334  ringrghm  20335  gsumdixp  20339  pwspjmhmmgpd  20348  pwsgprod  20350  lmodvsghm  20963  gsumfsum  21459  regsumfsum  21460  expmhm  21461  expghm  21500  evpmodpmf1o  21621  frlmgsum  21797  frlmsplit2  21798  frlmphl  21806  uvcff  21816  uvcresum  21818  snifpsrbag  21945  psrass1lem  21958  rhmpsrlem1  21965  rhmpsrlem2  21966  psrmulcllem  21970  psrlidm  21986  psrridm  21987  psrcom  21992  resspsrmul  22000  mvrf  22009  mplmon  22061  mplmonmul  22062  mplcoe1  22063  mplcoe5lem  22065  mplcoe5  22066  mplbas2  22068  psrbagsn  22089  evlslem4  22102  evlslem2  22105  evlslem3  22106  evlslem6  22107  evlslem1  22108  evlsval2  22113  evlsval3  22115  evlsvvvallem  22117  evlsvvval  22119  selvvvval  22168  psdcl  22199  psdmplcl  22200  psdmul  22204  psropprmul  22272  coe1mul2  22305  coe1tmmul2  22312  coe1tmmul  22313  ply1coe  22334  gsumsmonply1  22343  gsummoncoe1  22344  mamulid  22474  mamurid  22475  mdetunilem9  22653  mdetuni0  22654  mdetmul  22656  smadiadetlem3lem1  22699  m2cpmfo  22789  pmatcollpw1  22809  pmatcollpw3lem  22816  pmatcollpw3fi1lem2  22820  pm2mpcl  22830  mply1topmatcl  22838  mp2pm2mplem2  22840  mp2pm2mp  22844  pm2mpmhmlem2  22852  cayhamlem4  22921  pptbas  23041  tgrest  23192  resttopon  23194  rest0  23202  restfpw  23212  ordtbaslem  23221  ordtuni  23223  ordtrest  23235  cnpfval  23267  pnrmopn  23376  cncmp  23425  discmp  23431  1stcfb  23478  2ndcomap  23491  dis2ndc  23493  comppfsc  23565  kgencmp  23578  ptpjpre1  23604  ptpjcn  23644  ptcldmpt  23647  ptclsg  23648  dfac14  23651  xkoccn  23652  txcnp  23653  ptcnp  23655  uptx  23658  ptcn  23660  ptrescn  23672  xkoptsub  23687  xkoco1cn  23690  xkoco2cn  23691  cnmpt11  23696  pt1hmeo  23839  fbasrn  23917  trfilss  23922  trfg  23924  rnelfmlem  23985  flfcnp2  24040  fclscmpi  24062  alexsublem  24077  ptcmplem3  24087  symgtgp  24139  subgntr  24140  opnsubg  24141  clsnsg  24143  tgpconncomp  24146  eltsms  24166  haustsms  24169  tsmscls  24171  tsms0  24175  tsmsmhm  24179  tgptsmscls  24183  tsmssplit  24185  tsmsxplem1  24186  tsmsxplem2  24187  prdsdsf  24400  prdsxmetlem  24401  imasdsf1olem  24406  prdsbl  24524  stdbdxmet  24548  met1stc  24554  xrge0gsumle  24867  xrge0tsms  24868  cncfmpt2ss  24951  cnmptre  24962  evth  24994  evth2  24995  tcphcph  25272  rrxmval  25440  minveclem1  25459  minveclem3b  25463  iunmbl  25588  uniioombllem3  25620  ismbfcn2  25673  mbfeqalem1  25676  mbfeqalem2  25677  mbfss  25681  mbfmulc2re  25683  mbfneg  25685  mbfpos  25686  mbfposr  25687  mbfposb  25688  mbfadd  25696  mbfmulc2  25698  mbfsup  25699  mbfinf  25700  mbflimsup  25701  mbflimlem  25702  mbflim  25703  itg1climres  25749  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  mbfi1flimlem  25757  mbfi1flim  25758  mbfmullem2  25759  mbfmul  25761  itg2const2  25776  itg2seq  25777  itg2monolem1  25785  itg2monolem2  25786  itg2monolem3  25787  itg2mono  25788  itg2gt0  25795  itg2cnlem1  25796  itg2cnlem2  25797  itg2cn  25798  iblss  25840  itgitg1  25844  itgle  25845  itgeqa  25849  itgss3  25850  ibladdlem  25855  itgaddlem1  25858  iblabslem  25863  iblabs  25864  iblabsr  25865  iblmulc2  25866  itgmulc2lem1  25867  bddmulibl  25874  bddiblnc  25877  itggt0  25879  itgcn  25880  ellimc2  25912  limcmpt  25918  limcres  25921  limccnp  25926  limccnp2  25927  limcco  25928  perfdvf  25938  dvcnp2  25955  dvaddbr  25973  dvmulbr  25974  dvcjbr  25984  dvexp  25988  dvrec  25990  dvmptres3  25991  dvmptadd  25995  dvmptmul  25996  dvmptres2  25997  dvmptcmul  25999  dvmptcj  26003  dvmptntr  26006  dvmptco  26007  dvcnvlem  26011  dvef  26015  dvferm1  26020  dvferm2  26022  rolle  26025  dvlipcn  26029  dvle  26042  dvivth  26045  lhop1lem  26048  lhop1  26049  lhop2  26050  lhop  26051  dvfsumle  26056  dvfsumge  26057  dvmptrecl  26059  dvfsumlem2  26062  itgsubstlem  26083  itgpowd  26085  tdeglem4  26093  coe1mul3  26132  elply2  26229  plyf  26231  elplyd  26235  plypf1  26245  coeeq2  26275  coemullem  26283  coe1termlem  26291  dvply2g  26319  elqaalem2  26354  taylfvallem  26391  taylf  26394  tayl0  26395  taylpfval  26398  taylthlem1  26406  taylthlem2  26407  ulmcau  26428  ulmss  26430  ulmdvlem3  26435  mtest  26437  mtestbdd  26438  itgulm2  26442  dvradcnv  26454  pserulm  26455  pserdvlem2  26461  abelthlem9  26473  pige3ALT  26555  logtayl  26695  logccv  26698  loglesqrt  26796  leibpi  26977  rlimcnp  27000  rlimcnp2  27001  xrlimcnp  27003  efrlim  27004  dfef2  27005  o1cxp  27009  cxp2lim  27011  amgmlem  27024  lgamgulmlem2  27064  lgamgulmlem6  27068  lgamcvg2  27089  regamcl  27095  relgamcl  27096  basellem2  27116  basellem3  27117  sqff1o  27216  fsumvma  27247  dchrelbasd  27273  lgseisenlem3  27411  lgseisenlem4  27412  chpo1ub  27514  dchrisum0lem2a  27551  logsqvma2  27577  pnt2  27647  pnt  27648  incistruhgr  29219  minvecolem1  31016  hoaddcl  31900  homulcl  31901  cofmpt2  32779  mptiffisupp  32838  fpwrelmap  32878  gsummpt2d  33183  gsummptfsres  33188  gsummptf1od  33189  gsummptfsf1o  33194  gsumfs2d  33195  gsumzrsum  33199  gsummulsubdishift2  33203  gsummulsubdishift1s  33204  gsummulsubdishift2s  33205  xrge0tsmsd  33207  gsumwrd2dccat  33212  gsumvsca1  33360  gsumvsca2  33361  elrgspnlem1  33377  elrgspnlem2  33378  elrgspnlem3  33379  elrgspnlem4  33380  elrgspn  33381  elrgspnsubrunlem2  33383  elrspunidl  33568  elrspunsn  33569  ressply1evls1  33715  evl1deg2  33727  deg1prod  33733  selvascl  33768  selvply1rhmlem1  33771  extvfvcl  33787  evlextv  33793  mplvrpmga  33796  psrgsum  33799  psrmon  33800  psrmonmul  33801  psrmonprod  33803  esplyfvaln  33825  vietadeg1  33829  fedgmullem1  33880  fedgmullem2  33881  evls1fldgencl  33921  fldextrspunlsplem  33924  fldextrspunlsp  33925  extdgfialglem2  33944  ordtrestNEW  34172  esumf1o  34301  esumadd  34308  esumcst  34314  esumpfinval  34326  esumpcvgval  34329  esumcvg  34337  esumsup  34340  measinb  34472  measdivcst  34475  sitgclg  34593  dstfrvclim1  34729  gsumncl  34791  gsumnunsn  34792  fdvneggt  34851  fdvnegge  34853  itgexpif  34857  logdivsqrle  34901  indispconn  35532  cvxpconn  35540  cvmsss2  35572  cvmliftlem6  35588  cvmliftlem8  35590  mrsubcv  35808  mrsubff  35810  mrsubrn  35811  mrsubccat  35816  elmrsubrn  35818  msubrn  35827  msubff  35828  divcnvlin  36031  faclimlem2  36042  faclim  36044  faclim2  36046  knoppcnlem5  36883  knoppcnlem8  36886  knoppcnlem10  36888  knoppcnlem11  36889  curf  38045  finixpnum  38052  matunitlindflem1  38063  matunitlindflem2  38064  ptrest  38066  poimirlem17  38084  poimirlem20  38087  poimirlem24  38091  poimirlem30  38097  broucube  38101  mblfinlem2  38105  volsupnfl  38112  mbfposadd  38114  itg2addnclem2  38119  itg2gt0cn  38122  ibladdnclem  38123  itgaddnclem1  38125  itgaddnc  38127  iblabsnclem  38130  iblabsnc  38131  iblmulc2nc  38132  itgmulc2nclem1  38133  itgmulc2nclem2  38134  itgmulc2nc  38135  itgabsnc  38136  itggt0cn  38137  ftc1cnnc  38139  ftc1anclem1  38140  ftc1anclem2  38141  ftc1anclem3  38142  ftc1anclem4  38143  ftc1anclem5  38144  ftc1anclem6  38145  ftc1anclem7  38146  ftc1anclem8  38147  ftc1anc  38148  areacirclem4  38158  upixp  38176  totbndbnd  38236  prdsbnd  38240  cntotbnd  38243  rrnequiv  38282  lsatlss  39568  tendoplcl  41353  tendoicl  41368  aks4d1p1p5  42640  aks4d1p9  42653  hashscontpow  42687  sticksstones10  42720  sticksstones17  42728  sticksstones18  42729  unitscyglem1  42760  redvmptabs  42917  fimgmcyc  43100  evlsbagval  43116  evlselv  43119  fsuppind  43120  fsuppssind  43123  mhpind  43124  evlsmhpvvval  43125  mhphflem  43126  cmpfiiin  43226  mzpclall  43256  mzpindd  43275  fphpdo  43342  dnnumch3  43572  kelac1  43588  dfac21  43591  cantnfresb  43849  cantnf2  43850  tfsconcatrev  43873  rfovcnvf1od  44528  fsovfd  44536  fsovcnvlem  44537  clsk3nimkb  44564  mnringmulrcld  44752  expgrowth  44859  mptelpm  45702  mapss2  45730  monoord2xrv  46005  expcnfg  46115  clim1fr1  46125  sumnnodd  46154  limsupvaluz2  46260  supcnvlimsup  46262  climliminflimsupd  46323  liminfltlem  46326  cncfmptssg  46393  cncfcompt  46405  cxpcncf2  46421  dvsinax  46435  fperdvper  46441  dvcosax  46448  dvnmptdivc  46460  dvnprodlem2  46469  dvnprodlem3  46470  iblsplit  46488  itgcoscmulx  46491  itgiccshift  46502  itgperiod  46503  itgsbtaddcnst  46504  dirkerf  46619  dirkeritg  46624  hoidmvlelem1  47117  hoidmvlelem5  47121  ovnhoilem1  47123  ovnhoilem2  47124  ovnlecvr2  47132  ovncvr2  47133  hoidifhspf  47140  hspmbllem2  47149  opnvonmbllem2  47155  iccvonmbllem  47200  vonioolem1  47202  vonioolem2  47203  vonicclem1  47205  vonicclem2  47206  smfid  47274  cfsetsnfsetf  47600  funcringcsetcALTV2lem3  48862  funcringcsetclem3ALTV  48885  gsumlsscl  48950  ply1mulgsum  48960  lincfsuppcl  48983  linccl  48984  lincsum  48999  lincscmcl  49002  lcoss  49006  lincext1  49024  el0ldep  49036  lincresunit1  49047  lincresunit3  49051  lmod1zr  49063  fdivmptf  49111  refdivmptf  49112  1arymaptf  49211  aacllem  50370  amgmwlem  50371