Theorem fmpttd 7090

Description: Version of fmptd 7089 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 7089	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ↦ cmpt 5191  ⟶wf 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  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 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-fun 6516  df-fn 6517  df-f 6518

This theorem is referenced by:  fmpt3d  7091  fliftrel  7286  fsetfocdm  8837  pw2f1olem  9050  mapxpen  9113  fsuppssov1  9342  fsuppmptif  9357  wdom2d  9540  cantnflem1d  9648  cantnflem1  9649  ac5num  9996  acni2  10006  infpwfien  10022  fin23lem39  10310  fin1a2lem12  10371  canthp1lem2  10613  wuncval2  10707  gruf  10771  monoord2  14005  seqf1o  14015  ccatcl  14546  swrdcl  14617  swrdwrdsymb  14634  revcl  14733  revlen  14734  ello1mpt  15494  lo1o12  15506  lo1eq  15541  rlimeq  15542  climmpt2  15546  climrecl  15556  climge0  15557  o1compt  15560  rlimcn1b  15562  rlimdiv  15619  isercoll2  15642  caurcvg2  15651  fsumf1o  15696  sumss  15697  fsumss  15698  fsumcl2lem  15704  fsumadd  15713  isumclim3  15732  isummulc2  15735  fsummulc2  15757  fsumrelem  15780  climfsum  15793  isumshft  15812  divcnv  15826  prodfdiv  15869  fprodf1o  15919  prodss  15920  fprodss  15921  fprodser  15922  fprodcl2lem  15923  fprodmul  15933  fproddiv  15934  fprodn0  15952  iprodclim3  15973  fprodefsum  16068  iserodd  16813  prmreclem2  16895  vdwapf  16950  vdwlem4  16962  ramcl  17007  prmodvdslcmf  17025  prdsplusg  17428  prdsmulr  17429  prdsvsca  17430  mrcflem  17574  mreacs  17626  acsfn  17627  hofcllem  18226  hofcl  18227  yonedalem3a  18242  yonedalem4c  18245  yonedainv  18249  prdspjmhm  18763  pwsco1mhm  18766  pwsco2mhm  18767  gsumz  18770  gsumwspan  18780  odf1o1  19509  odf1o2  19510  sylow2blem1  19557  mulgmhm  19764  mulgghm  19765  iscyggen2  19818  cyggenod  19821  iscyg3  19823  gsumzsplit  19864  gsumsplit2  19866  gsumconst  19871  gsummptshft  19873  gsummhm2  19876  gsummptmhm  19877  gsummptf1o  19900  gsum2dlem1  19907  gsum2dlem2  19908  gsum2d  19909  prdsgsum  19918  dprdfeq0  19961  dprdlub  19965  dprdz  19969  dprd2dlem1  19980  dprd2da  19981  srglmhm  20137  srgrmhm  20138  ringlghm  20228  ringrghm  20229  gsumdixp  20235  pwspjmhmmgpd  20244  lmodvsghm  20836  gsumfsum  21358  regsumfsum  21359  expmhm  21360  expghm  21392  evpmodpmf1o  21512  frlmgsum  21688  frlmsplit2  21689  frlmphl  21697  uvcff  21707  uvcresum  21709  snifpsrbag  21836  psrass1lem  21848  rhmpsrlem1  21856  rhmpsrlem2  21857  psrmulcllem  21861  psrlidm  21878  psrridm  21879  psrcom  21884  resspsrmul  21892  mvrf  21901  mplmon  21949  mplmonmul  21950  mplcoe1  21951  mplcoe5lem  21953  mplcoe5  21954  mplbas2  21956  psrbagsn  21977  evlslem4  21990  evlslem2  21993  evlslem3  21994  evlslem6  21995  evlslem1  21996  evlsval2  22001  psdcl  22055  psdmplcl  22056  psdmul  22060  psropprmul  22129  coe1mul2  22162  coe1tmmul2  22169  coe1tmmul  22170  ply1coe  22192  gsumsmonply1  22201  gsummoncoe1  22202  mamulid  22335  mamurid  22336  mdetunilem9  22514  mdetuni0  22515  mdetmul  22517  smadiadetlem3lem1  22560  m2cpmfo  22650  pmatcollpw1  22670  pmatcollpw3lem  22677  pmatcollpw3fi1lem2  22681  pm2mpcl  22691  mply1topmatcl  22699  mp2pm2mplem2  22701  mp2pm2mp  22705  pm2mpmhmlem2  22713  cayhamlem4  22782  pptbas  22902  tgrest  23053  resttopon  23055  rest0  23063  restfpw  23073  ordtbaslem  23082  ordtuni  23084  ordtrest  23096  cnpfval  23128  pnrmopn  23237  cncmp  23286  discmp  23292  1stcfb  23339  2ndcomap  23352  dis2ndc  23354  comppfsc  23426  kgencmp  23439  ptpjpre1  23465  ptpjcn  23505  ptcldmpt  23508  ptclsg  23509  dfac14  23512  xkoccn  23513  txcnp  23514  ptcnp  23516  uptx  23519  ptcn  23521  ptrescn  23533  xkoptsub  23548  xkoco1cn  23551  xkoco2cn  23552  cnmpt11  23557  pt1hmeo  23700  fbasrn  23778  trfilss  23783  trfg  23785  rnelfmlem  23846  flfcnp2  23901  fclscmpi  23923  alexsublem  23938  ptcmplem3  23948  symgtgp  24000  subgntr  24001  opnsubg  24002  clsnsg  24004  tgpconncomp  24007  eltsms  24027  haustsms  24030  tsmscls  24032  tsms0  24036  tsmsmhm  24040  tgptsmscls  24044  tsmssplit  24046  tsmsxplem1  24047  tsmsxplem2  24048  prdsdsf  24262  prdsxmetlem  24263  imasdsf1olem  24268  prdsbl  24386  stdbdxmet  24410  met1stc  24416  xrge0gsumle  24729  xrge0tsms  24730  cncfmpt2ss  24816  cnmptre  24828  evth  24865  evth2  24866  tcphcph  25144  rrxmval  25312  minveclem1  25331  minveclem3b  25335  iunmbl  25461  uniioombllem3  25493  ismbfcn2  25546  mbfeqalem1  25549  mbfeqalem2  25550  mbfss  25554  mbfmulc2re  25556  mbfneg  25558  mbfpos  25559  mbfposr  25560  mbfposb  25561  mbfadd  25569  mbfmulc2  25571  mbfsup  25572  mbfinf  25573  mbflimsup  25574  mbflimlem  25575  mbflim  25576  itg1climres  25622  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  mbfi1flimlem  25630  mbfi1flim  25631  mbfmullem2  25632  mbfmul  25634  itg2const2  25649  itg2seq  25650  itg2monolem1  25658  itg2monolem2  25659  itg2monolem3  25660  itg2mono  25661  itg2gt0  25668  itg2cnlem1  25669  itg2cnlem2  25670  itg2cn  25671  iblss  25713  itgitg1  25717  itgle  25718  itgeqa  25722  itgss3  25723  ibladdlem  25728  itgaddlem1  25731  iblabslem  25736  iblabs  25737  iblabsr  25738  iblmulc2  25739  itgmulc2lem1  25740  bddmulibl  25747  bddiblnc  25750  itggt0  25752  itgcn  25753  ellimc2  25785  limcmpt  25791  limcres  25794  limccnp  25799  limccnp2  25800  limcco  25801  perfdvf  25811  dvcnp2  25828  dvcnp2OLD  25829  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvcjbr  25860  dvexp  25864  dvrec  25866  dvmptres3  25867  dvmptadd  25871  dvmptmul  25872  dvmptres2  25873  dvmptcmul  25875  dvmptcj  25879  dvmptntr  25882  dvmptco  25883  dvcnvlem  25887  dvef  25891  dvferm1  25896  dvferm2  25898  rolle  25901  dvlipcn  25906  dvle  25919  dvivth  25922  lhop1lem  25925  lhop1  25926  lhop2  25927  lhop  25928  dvfsumle  25933  dvfsumleOLD  25934  dvfsumge  25935  dvmptrecl  25937  dvfsumlem2  25940  dvfsumlem2OLD  25941  itgsubstlem  25962  itgpowd  25964  tdeglem4  25972  coe1mul3  26011  elply2  26108  plyf  26110  elplyd  26114  plypf1  26124  coeeq2  26154  coemullem  26162  coe1termlem  26170  dvply2g  26199  dvply2gOLD  26200  elqaalem2  26235  taylfvallem  26272  taylf  26275  tayl0  26276  taylpfval  26279  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  ulmcau  26311  ulmss  26313  ulmdvlem3  26318  mtest  26320  mtestbdd  26321  itgulm2  26325  dvradcnv  26337  pserulm  26338  pserdvlem2  26345  abelthlem9  26357  pige3ALT  26436  logtayl  26576  logccv  26579  loglesqrt  26678  leibpi  26859  rlimcnp  26882  rlimcnp2  26883  xrlimcnp  26885  efrlim  26886  efrlimOLD  26887  dfef2  26888  o1cxp  26892  cxp2lim  26894  amgmlem  26907  lgamgulmlem2  26947  lgamgulmlem6  26951  lgamcvg2  26972  regamcl  26978  relgamcl  26979  basellem2  26999  basellem3  27000  sqff1o  27099  fsumvma  27131  dchrelbasd  27157  lgseisenlem3  27295  lgseisenlem4  27296  chpo1ub  27398  dchrisum0lem2a  27435  logsqvma2  27461  pnt2  27531  pnt  27532  incistruhgr  29013  minvecolem1  30810  hoaddcl  31694  homulcl  31695  cofmpt2  32565  mptiffisupp  32623  fpwrelmap  32663  gsummpt2d  32996  gsummptfsf1o  33001  gsumfs2d  33002  gsumzrsum  33006  xrge0tsmsd  33009  gsumwrd2dccat  33014  gsumvsca1  33186  gsumvsca2  33187  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem3  33202  elrgspnlem4  33203  elrgspn  33204  elrgspnsubrunlem2  33206  elrspunidl  33406  elrspunsn  33407  ressply1evls1  33541  evl1deg2  33553  fedgmullem1  33632  fedgmullem2  33633  evls1fldgencl  33672  fldextrspunlsplem  33675  fldextrspunlsp  33676  ordtrestNEW  33918  esumf1o  34047  esumadd  34054  esumcst  34060  esumpfinval  34072  esumpcvgval  34075  esumcvg  34083  esumsup  34086  measinb  34218  measdivcst  34221  sitgclg  34340  dstfrvclim1  34476  gsumncl  34538  gsumnunsn  34539  fdvneggt  34598  fdvnegge  34600  itgexpif  34604  logdivsqrle  34648  indispconn  35228  cvxpconn  35236  cvmsss2  35268  cvmliftlem6  35284  cvmliftlem8  35286  mrsubcv  35504  mrsubff  35506  mrsubrn  35507  mrsubccat  35512  elmrsubrn  35514  msubrn  35523  msubff  35524  divcnvlin  35727  faclimlem2  35738  faclim  35740  faclim2  35742  knoppcnlem5  36492  knoppcnlem8  36495  knoppcnlem10  36497  knoppcnlem11  36498  curf  37599  finixpnum  37606  matunitlindflem1  37617  matunitlindflem2  37618  ptrest  37620  poimirlem17  37638  poimirlem20  37641  poimirlem24  37645  poimirlem30  37651  broucube  37655  mblfinlem2  37659  volsupnfl  37666  mbfposadd  37668  itg2addnclem2  37673  itg2gt0cn  37676  ibladdnclem  37677  itgaddnclem1  37679  itgaddnc  37681  iblabsnclem  37684  iblabsnc  37685  iblmulc2nc  37686  itgmulc2nclem1  37687  itgmulc2nclem2  37688  itgmulc2nc  37689  itgabsnc  37690  itggt0cn  37691  ftc1cnnc  37693  ftc1anclem1  37694  ftc1anclem2  37695  ftc1anclem3  37696  ftc1anclem4  37697  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  areacirclem4  37712  upixp  37730  totbndbnd  37790  prdsbnd  37794  cntotbnd  37797  rrnequiv  37836  lsatlss  38996  tendoplcl  40782  tendoicl  40797  aks4d1p1p5  42070  aks4d1p9  42083  hashscontpow  42117  sticksstones10  42150  sticksstones17  42158  sticksstones18  42159  unitscyglem1  42190  redvmptabs  42355  fimgmcyc  42529  pwsgprod  42539  evlsval3  42554  evlsvvvallem  42556  evlsvvval  42558  evlsbagval  42561  selvvvval  42580  evlselv  42582  fsuppind  42585  fsuppssind  42588  mhpind  42589  evlsmhpvvval  42590  mhphflem  42591  cmpfiiin  42692  mzpclall  42722  mzpindd  42741  fphpdo  42812  dnnumch3  43043  kelac1  43059  dfac21  43062  cantnfresb  43320  cantnf2  43321  tfsconcatrev  43344  rfovcnvf1od  44000  fsovfd  44008  fsovcnvlem  44009  clsk3nimkb  44036  mnringmulrcld  44224  expgrowth  44331  mptelpm  45177  mapss2  45206  monoord2xrv  45486  expcnfg  45596  clim1fr1  45606  sumnnodd  45635  limsupvaluz2  45743  supcnvlimsup  45745  climliminflimsupd  45806  liminfltlem  45809  cncfmptssg  45876  cncfcompt  45888  cxpcncf2  45904  dvsinax  45918  fperdvper  45924  dvcosax  45931  dvnmptdivc  45943  dvnprodlem2  45952  dvnprodlem3  45953  iblsplit  45971  itgcoscmulx  45974  itgiccshift  45985  itgperiod  45986  itgsbtaddcnst  45987  dirkerf  46102  dirkeritg  46107  hoidmvlelem1  46600  hoidmvlelem5  46604  ovnhoilem1  46606  ovnhoilem2  46607  ovnlecvr2  46615  ovncvr2  46616  hoidifhspf  46623  hspmbllem2  46632  opnvonmbllem2  46638  iccvonmbllem  46683  vonioolem1  46685  vonioolem2  46686  vonicclem1  46688  vonicclem2  46689  smfid  46757  cfsetsnfsetf  47063  funcringcsetcALTV2lem3  48284  funcringcsetclem3ALTV  48307  gsumlsscl  48372  ply1mulgsum  48383  lincfsuppcl  48406  linccl  48407  lincsum  48422  lincscmcl  48425  lcoss  48429  lincext1  48447  el0ldep  48459  lincresunit1  48470  lincresunit3  48474  lmod1zr  48486  fdivmptf  48534  refdivmptf  48535  1arymaptf  48634  aacllem  49794  amgmwlem  49795