Theorem fmpttd 7043

Description: Version of fmptd 7042 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 2730	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	1, 2	fmptd 7042	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2110   ↦ cmpt 5170  ⟶wf 6473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-fun 6479  df-fn 6480  df-f 6481

This theorem is referenced by:  fmpt3d  7044  fliftrel  7237  fsetfocdm  8780  pw2f1olem  8989  mapxpen  9051  fsuppssov1  9263  fsuppmptif  9278  wdom2d  9461  cantnflem1d  9573  cantnflem1  9574  ac5num  9919  acni2  9929  infpwfien  9945  fin23lem39  10233  fin1a2lem12  10294  canthp1lem2  10536  wuncval2  10630  gruf  10694  monoord2  13932  seqf1o  13942  ccatcl  14473  swrdcl  14545  swrdwrdsymb  14562  revcl  14660  revlen  14661  ello1mpt  15420  lo1o12  15432  lo1eq  15467  rlimeq  15468  climmpt2  15472  climrecl  15482  climge0  15483  o1compt  15486  rlimcn1b  15488  rlimdiv  15545  isercoll2  15568  caurcvg2  15577  fsumf1o  15622  sumss  15623  fsumss  15624  fsumcl2lem  15630  fsumadd  15639  isumclim3  15658  isummulc2  15661  fsummulc2  15683  fsumrelem  15706  climfsum  15719  isumshft  15738  divcnv  15752  prodfdiv  15795  fprodf1o  15845  prodss  15846  fprodss  15847  fprodser  15848  fprodcl2lem  15849  fprodmul  15859  fproddiv  15860  fprodn0  15878  iprodclim3  15899  fprodefsum  15994  iserodd  16739  prmreclem2  16821  vdwapf  16876  vdwlem4  16888  ramcl  16933  prmodvdslcmf  16951  prdsplusg  17354  prdsmulr  17355  prdsvsca  17356  mrcflem  17504  mreacs  17556  acsfn  17557  hofcllem  18156  hofcl  18157  yonedalem3a  18172  yonedalem4c  18175  yonedainv  18179  prdspjmhm  18729  pwsco1mhm  18732  pwsco2mhm  18733  gsumz  18736  gsumwspan  18746  odf1o1  19477  odf1o2  19478  sylow2blem1  19525  mulgmhm  19732  mulgghm  19733  iscyggen2  19786  cyggenod  19789  iscyg3  19791  gsumzsplit  19832  gsumsplit2  19834  gsumconst  19839  gsummptshft  19841  gsummhm2  19844  gsummptmhm  19845  gsummptf1o  19868  gsum2dlem1  19875  gsum2dlem2  19876  gsum2d  19877  prdsgsum  19886  dprdfeq0  19929  dprdlub  19933  dprdz  19937  dprd2dlem1  19948  dprd2da  19949  srglmhm  20132  srgrmhm  20133  ringlghm  20223  ringrghm  20224  gsumdixp  20230  pwspjmhmmgpd  20239  lmodvsghm  20849  gsumfsum  21364  regsumfsum  21365  expmhm  21366  expghm  21405  evpmodpmf1o  21526  frlmgsum  21702  frlmsplit2  21703  frlmphl  21711  uvcff  21721  uvcresum  21723  snifpsrbag  21850  psrass1lem  21862  rhmpsrlem1  21870  rhmpsrlem2  21871  psrmulcllem  21875  psrlidm  21892  psrridm  21893  psrcom  21898  resspsrmul  21906  mvrf  21915  mplmon  21963  mplmonmul  21964  mplcoe1  21965  mplcoe5lem  21967  mplcoe5  21968  mplbas2  21970  psrbagsn  21991  evlslem4  22004  evlslem2  22007  evlslem3  22008  evlslem6  22009  evlslem1  22010  evlsval2  22015  psdcl  22069  psdmplcl  22070  psdmul  22074  psropprmul  22143  coe1mul2  22176  coe1tmmul2  22183  coe1tmmul  22184  ply1coe  22206  gsumsmonply1  22215  gsummoncoe1  22216  mamulid  22349  mamurid  22350  mdetunilem9  22528  mdetuni0  22529  mdetmul  22531  smadiadetlem3lem1  22574  m2cpmfo  22664  pmatcollpw1  22684  pmatcollpw3lem  22691  pmatcollpw3fi1lem2  22695  pm2mpcl  22705  mply1topmatcl  22713  mp2pm2mplem2  22715  mp2pm2mp  22719  pm2mpmhmlem2  22727  cayhamlem4  22796  pptbas  22916  tgrest  23067  resttopon  23069  rest0  23077  restfpw  23087  ordtbaslem  23096  ordtuni  23098  ordtrest  23110  cnpfval  23142  pnrmopn  23251  cncmp  23300  discmp  23306  1stcfb  23353  2ndcomap  23366  dis2ndc  23368  comppfsc  23440  kgencmp  23453  ptpjpre1  23479  ptpjcn  23519  ptcldmpt  23522  ptclsg  23523  dfac14  23526  xkoccn  23527  txcnp  23528  ptcnp  23530  uptx  23533  ptcn  23535  ptrescn  23547  xkoptsub  23562  xkoco1cn  23565  xkoco2cn  23566  cnmpt11  23571  pt1hmeo  23714  fbasrn  23792  trfilss  23797  trfg  23799  rnelfmlem  23860  flfcnp2  23915  fclscmpi  23937  alexsublem  23952  ptcmplem3  23962  symgtgp  24014  subgntr  24015  opnsubg  24016  clsnsg  24018  tgpconncomp  24021  eltsms  24041  haustsms  24044  tsmscls  24046  tsms0  24050  tsmsmhm  24054  tgptsmscls  24058  tsmssplit  24060  tsmsxplem1  24061  tsmsxplem2  24062  prdsdsf  24275  prdsxmetlem  24276  imasdsf1olem  24281  prdsbl  24399  stdbdxmet  24423  met1stc  24429  xrge0gsumle  24742  xrge0tsms  24743  cncfmpt2ss  24829  cnmptre  24841  evth  24878  evth2  24879  tcphcph  25157  rrxmval  25325  minveclem1  25344  minveclem3b  25348  iunmbl  25474  uniioombllem3  25506  ismbfcn2  25559  mbfeqalem1  25562  mbfeqalem2  25563  mbfss  25567  mbfmulc2re  25569  mbfneg  25571  mbfpos  25572  mbfposr  25573  mbfposb  25574  mbfadd  25582  mbfmulc2  25584  mbfsup  25585  mbfinf  25586  mbflimsup  25587  mbflimlem  25588  mbflim  25589  itg1climres  25635  mbfi1fseqlem3  25638  mbfi1fseqlem4  25639  mbfi1flimlem  25643  mbfi1flim  25644  mbfmullem2  25645  mbfmul  25647  itg2const2  25662  itg2seq  25663  itg2monolem1  25671  itg2monolem2  25672  itg2monolem3  25673  itg2mono  25674  itg2gt0  25681  itg2cnlem1  25682  itg2cnlem2  25683  itg2cn  25684  iblss  25726  itgitg1  25730  itgle  25731  itgeqa  25735  itgss3  25736  ibladdlem  25741  itgaddlem1  25744  iblabslem  25749  iblabs  25750  iblabsr  25751  iblmulc2  25752  itgmulc2lem1  25753  bddmulibl  25760  bddiblnc  25763  itggt0  25765  itgcn  25766  ellimc2  25798  limcmpt  25804  limcres  25807  limccnp  25812  limccnp2  25813  limcco  25814  perfdvf  25824  dvcnp2  25841  dvcnp2OLD  25842  dvaddbr  25860  dvmulbr  25861  dvmulbrOLD  25862  dvcjbr  25873  dvexp  25877  dvrec  25879  dvmptres3  25880  dvmptadd  25884  dvmptmul  25885  dvmptres2  25886  dvmptcmul  25888  dvmptcj  25892  dvmptntr  25895  dvmptco  25896  dvcnvlem  25900  dvef  25904  dvferm1  25909  dvferm2  25911  rolle  25914  dvlipcn  25919  dvle  25932  dvivth  25935  lhop1lem  25938  lhop1  25939  lhop2  25940  lhop  25941  dvfsumle  25946  dvfsumleOLD  25947  dvfsumge  25948  dvmptrecl  25950  dvfsumlem2  25953  dvfsumlem2OLD  25954  itgsubstlem  25975  itgpowd  25977  tdeglem4  25985  coe1mul3  26024  elply2  26121  plyf  26123  elplyd  26127  plypf1  26137  coeeq2  26167  coemullem  26175  coe1termlem  26183  dvply2g  26212  dvply2gOLD  26213  elqaalem2  26248  taylfvallem  26285  taylf  26288  tayl0  26289  taylpfval  26292  taylthlem1  26301  taylthlem2  26302  taylthlem2OLD  26303  ulmcau  26324  ulmss  26326  ulmdvlem3  26331  mtest  26333  mtestbdd  26334  itgulm2  26338  dvradcnv  26350  pserulm  26351  pserdvlem2  26358  abelthlem9  26370  pige3ALT  26449  logtayl  26589  logccv  26592  loglesqrt  26691  leibpi  26872  rlimcnp  26895  rlimcnp2  26896  xrlimcnp  26898  efrlim  26899  efrlimOLD  26900  dfef2  26901  o1cxp  26905  cxp2lim  26907  amgmlem  26920  lgamgulmlem2  26960  lgamgulmlem6  26964  lgamcvg2  26985  regamcl  26991  relgamcl  26992  basellem2  27012  basellem3  27013  sqff1o  27112  fsumvma  27144  dchrelbasd  27170  lgseisenlem3  27308  lgseisenlem4  27309  chpo1ub  27411  dchrisum0lem2a  27448  logsqvma2  27474  pnt2  27544  pnt  27545  incistruhgr  29050  minvecolem1  30844  hoaddcl  31728  homulcl  31729  cofmpt2  32606  mptiffisupp  32664  fpwrelmap  32706  gsummpt2d  33019  gsummptfsf1o  33024  gsumfs2d  33025  gsumzrsum  33029  xrge0tsmsd  33032  gsumwrd2dccat  33037  gsumvsca1  33185  gsumvsca2  33186  elrgspnlem1  33199  elrgspnlem2  33200  elrgspnlem3  33201  elrgspnlem4  33202  elrgspn  33203  elrgspnsubrunlem2  33205  elrspunidl  33383  elrspunsn  33384  ressply1evls1  33518  evl1deg2  33530  mplvrpmga  33565  fedgmullem1  33632  fedgmullem2  33633  evls1fldgencl  33673  fldextrspunlsplem  33676  fldextrspunlsp  33677  extdgfialglem2  33696  ordtrestNEW  33924  esumf1o  34053  esumadd  34060  esumcst  34066  esumpfinval  34078  esumpcvgval  34081  esumcvg  34089  esumsup  34092  measinb  34224  measdivcst  34227  sitgclg  34345  dstfrvclim1  34481  gsumncl  34543  gsumnunsn  34544  fdvneggt  34603  fdvnegge  34605  itgexpif  34609  logdivsqrle  34653  indispconn  35246  cvxpconn  35254  cvmsss2  35286  cvmliftlem6  35302  cvmliftlem8  35304  mrsubcv  35522  mrsubff  35524  mrsubrn  35525  mrsubccat  35530  elmrsubrn  35532  msubrn  35541  msubff  35542  divcnvlin  35745  faclimlem2  35756  faclim  35758  faclim2  35760  knoppcnlem5  36510  knoppcnlem8  36513  knoppcnlem10  36515  knoppcnlem11  36516  curf  37617  finixpnum  37624  matunitlindflem1  37635  matunitlindflem2  37636  ptrest  37638  poimirlem17  37656  poimirlem20  37659  poimirlem24  37663  poimirlem30  37669  broucube  37673  mblfinlem2  37677  volsupnfl  37684  mbfposadd  37686  itg2addnclem2  37691  itg2gt0cn  37694  ibladdnclem  37695  itgaddnclem1  37697  itgaddnc  37699  iblabsnclem  37702  iblabsnc  37703  iblmulc2nc  37704  itgmulc2nclem1  37705  itgmulc2nclem2  37706  itgmulc2nc  37707  itgabsnc  37708  itggt0cn  37709  ftc1cnnc  37711  ftc1anclem1  37712  ftc1anclem2  37713  ftc1anclem3  37714  ftc1anclem4  37715  ftc1anclem5  37716  ftc1anclem6  37717  ftc1anclem7  37718  ftc1anclem8  37719  ftc1anc  37720  areacirclem4  37730  upixp  37748  totbndbnd  37808  prdsbnd  37812  cntotbnd  37815  rrnequiv  37854  lsatlss  39014  tendoplcl  40799  tendoicl  40814  aks4d1p1p5  42087  aks4d1p9  42100  hashscontpow  42134  sticksstones10  42167  sticksstones17  42175  sticksstones18  42176  unitscyglem1  42207  redvmptabs  42372  fimgmcyc  42546  pwsgprod  42556  evlsval3  42571  evlsvvvallem  42573  evlsvvval  42575  evlsbagval  42578  selvvvval  42597  evlselv  42599  fsuppind  42602  fsuppssind  42605  mhpind  42606  evlsmhpvvval  42607  mhphflem  42608  cmpfiiin  42709  mzpclall  42739  mzpindd  42758  fphpdo  42829  dnnumch3  43059  kelac1  43075  dfac21  43078  cantnfresb  43336  cantnf2  43337  tfsconcatrev  43360  rfovcnvf1od  44016  fsovfd  44024  fsovcnvlem  44025  clsk3nimkb  44052  mnringmulrcld  44240  expgrowth  44347  mptelpm  45192  mapss2  45221  monoord2xrv  45500  expcnfg  45610  clim1fr1  45620  sumnnodd  45649  limsupvaluz2  45755  supcnvlimsup  45757  climliminflimsupd  45818  liminfltlem  45821  cncfmptssg  45888  cncfcompt  45900  cxpcncf2  45916  dvsinax  45930  fperdvper  45936  dvcosax  45943  dvnmptdivc  45955  dvnprodlem2  45964  dvnprodlem3  45965  iblsplit  45983  itgcoscmulx  45986  itgiccshift  45997  itgperiod  45998  itgsbtaddcnst  45999  dirkerf  46114  dirkeritg  46119  hoidmvlelem1  46612  hoidmvlelem5  46616  ovnhoilem1  46618  ovnhoilem2  46619  ovnlecvr2  46627  ovncvr2  46628  hoidifhspf  46635  hspmbllem2  46644  opnvonmbllem2  46650  iccvonmbllem  46695  vonioolem1  46697  vonioolem2  46698  vonicclem1  46700  vonicclem2  46701  smfid  46769  cfsetsnfsetf  47068  funcringcsetcALTV2lem3  48302  funcringcsetclem3ALTV  48325  gsumlsscl  48390  ply1mulgsum  48401  lincfsuppcl  48424  linccl  48425  lincsum  48440  lincscmcl  48443  lcoss  48447  lincext1  48465  el0ldep  48477  lincresunit1  48488  lincresunit3  48492  lmod1zr  48504  fdivmptf  48552  refdivmptf  48553  1arymaptf  48652  aacllem  49812  amgmwlem  49813