Theorem fmpttd 6873

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2110   ↦ cmpt 5138  ⟶wf 6345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  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 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  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  6874  fliftrel  7055  pw2f1olem  8615  mapxpen  8677  fsuppmptif  8857  wdom2d  9038  cantnflem1d  9145  cantnflem1  9146  ac5num  9456  acni2  9466  infpwfien  9482  fin23lem39  9766  fin1a2lem12  9827  canthp1lem2  10069  wuncval2  10163  gruf  10227  monoord2  13395  seqf1o  13405  ccatcl  13920  swrdcl  14001  swrdwrdsymb  14018  revcl  14117  revlen  14118  ello1mpt  14872  lo1o12  14884  lo1eq  14919  rlimeq  14920  climmpt2  14924  climrecl  14934  climge0  14935  o1compt  14938  rlimcn1b  14940  rlimdiv  14996  isercoll2  15019  caurcvg2  15028  fsumf1o  15074  sumss  15075  fsumss  15076  fsumcl2lem  15082  fsumadd  15090  isumclim3  15108  isummulc2  15111  fsummulc2  15133  fsumrelem  15156  climfsum  15169  isumshft  15188  divcnv  15202  prodfdiv  15246  fprodf1o  15294  prodss  15295  fprodss  15296  fprodser  15297  fprodcl2lem  15298  fprodmul  15308  fproddiv  15309  fprodn0  15327  iprodclim3  15348  fprodefsum  15442  iserodd  16166  prmreclem2  16247  vdwapf  16302  vdwlem4  16314  ramcl  16359  prmodvdslcmf  16377  prdsplusg  16725  prdsmulr  16726  prdsvsca  16727  mrcflem  16871  mreacs  16923  acsfn  16924  hofcllem  17502  hofcl  17503  yonedalem3a  17518  yonedalem4c  17521  yonedainv  17525  prdspjmhm  17987  pwsco1mhm  17990  pwsco2mhm  17991  gsumz  17994  gsumwspan  18005  odf1o1  18691  odf1o2  18692  sylow2blem1  18739  mulgmhm  18942  mulgghm  18943  iscyggen2  18994  cyggenod  18997  iscyg3  18999  gsumzsplit  19041  gsumsplit2  19043  gsumconst  19048  gsummptshft  19050  gsummhm2  19053  gsummptmhm  19054  gsummptf1o  19077  gsum2dlem1  19084  gsum2dlem2  19085  gsum2d  19086  prdsgsum  19095  dprdfeq0  19138  dprdlub  19142  dprdz  19146  dprd2dlem1  19157  dprd2da  19158  srglmhm  19279  srgrmhm  19280  ringlghm  19348  ringrghm  19349  gsumdixp  19353  lmodvsghm  19689  snifpsrbag  20140  psrass1lem  20151  psrmulcllem  20161  psrlidm  20177  psrridm  20178  psrcom  20183  resspsrmul  20191  mvrf  20198  mplmon  20238  mplmonmul  20239  mplcoe1  20240  mplcoe5lem  20242  mplcoe5  20243  mplbas2  20245  psrbagsn  20269  evlslem4  20282  evlslem2  20286  evlslem3  20287  evlslem6  20288  evlslem1  20289  evlsval2  20294  psropprmul  20400  coe1mul2  20431  coe1tmmul2  20438  coe1tmmul  20439  ply1coe  20458  gsumsmonply1  20465  gsummoncoe1  20466  gsumfsum  20606  regsumfsum  20607  expmhm  20608  expghm  20637  evpmodpmf1o  20734  frlmgsum  20910  frlmsplit2  20911  frlmphl  20919  uvcff  20929  uvcresum  20931  mamulid  21044  mamurid  21045  mdetunilem9  21223  mdetuni0  21224  mdetmul  21226  smadiadetlem3lem1  21269  m2cpmfo  21358  pmatcollpw1  21378  pmatcollpw3lem  21385  pmatcollpw3fi1lem2  21389  pm2mpcl  21399  mply1topmatcl  21407  mp2pm2mplem2  21409  mp2pm2mp  21413  pm2mpmhmlem2  21421  cayhamlem4  21490  pptbas  21610  tgrest  21761  resttopon  21763  rest0  21771  restfpw  21781  ordtbaslem  21790  ordtuni  21792  ordtrest  21804  cnpfval  21836  pnrmopn  21945  cncmp  21994  discmp  22000  1stcfb  22047  2ndcomap  22060  dis2ndc  22062  comppfsc  22134  kgencmp  22147  ptpjpre1  22173  ptpjcn  22213  ptcldmpt  22216  ptclsg  22217  dfac14  22220  xkoccn  22221  txcnp  22222  ptcnp  22224  uptx  22227  ptcn  22229  ptrescn  22241  xkoptsub  22256  xkoco1cn  22259  xkoco2cn  22260  cnmpt11  22265  pt1hmeo  22408  fbasrn  22486  trfilss  22491  trfg  22493  rnelfmlem  22554  flfcnp2  22609  fclscmpi  22631  alexsublem  22646  ptcmplem3  22656  symgtgp  22708  subgntr  22709  opnsubg  22710  clsnsg  22712  tgpconncomp  22715  eltsms  22735  haustsms  22738  tsmscls  22740  tsms0  22744  tsmsmhm  22748  tgptsmscls  22752  tsmssplit  22754  tsmsxplem1  22755  tsmsxplem2  22756  prdsdsf  22971  prdsxmetlem  22972  imasdsf1olem  22977  prdsbl  23095  stdbdxmet  23119  met1stc  23125  xrge0gsumle  23435  xrge0tsms  23436  cncfmpt2ss  23517  cnmptre  23525  evth  23557  evth2  23558  tcphcph  23834  rrxmval  24002  minveclem1  24021  minveclem3b  24025  iunmbl  24148  uniioombllem3  24180  ismbfcn2  24233  mbfeqalem1  24236  mbfeqalem2  24237  mbfss  24241  mbfmulc2re  24243  mbfneg  24245  mbfpos  24246  mbfposr  24247  mbfposb  24248  mbfadd  24256  mbfmulc2  24258  mbfsup  24259  mbfinf  24260  mbflimsup  24261  mbflimlem  24262  mbflim  24263  itg1climres  24309  mbfi1fseqlem3  24312  mbfi1fseqlem4  24313  mbfi1flimlem  24317  mbfi1flim  24318  mbfmullem2  24319  mbfmul  24321  itg2const2  24336  itg2seq  24337  itg2monolem1  24345  itg2monolem2  24346  itg2monolem3  24347  itg2mono  24348  itg2gt0  24355  itg2cnlem1  24356  itg2cnlem2  24357  itg2cn  24358  iblss  24399  itgitg1  24403  itgle  24404  itgeqa  24408  itgss3  24409  ibladdlem  24414  itgaddlem1  24417  iblabslem  24422  iblabs  24423  iblabsr  24424  iblmulc2  24425  itgmulc2lem1  24426  bddmulibl  24433  itggt0  24436  itgcn  24437  ellimc2  24469  limcmpt  24475  limcres  24478  limccnp  24483  limccnp2  24484  limcco  24485  perfdvf  24495  dvcnp2  24511  dvaddbr  24529  dvmulbr  24530  dvcjbr  24540  dvexp  24544  dvrec  24546  dvmptres3  24547  dvmptadd  24551  dvmptmul  24552  dvmptres2  24553  dvmptcmul  24555  dvmptcj  24559  dvmptntr  24562  dvmptco  24563  dvcnvlem  24567  dvef  24571  dvferm1  24576  dvferm2  24578  rolle  24581  dvlipcn  24585  dvle  24598  dvivth  24601  lhop1lem  24604  lhop1  24605  lhop2  24606  lhop  24607  dvfsumle  24612  dvfsumge  24613  dvmptrecl  24615  dvfsumlem2  24618  itgsubstlem  24639  tdeglem4  24648  coe1mul3  24687  elply2  24780  plyf  24782  elplyd  24786  plypf1  24796  coeeq2  24826  coemullem  24834  coe1termlem  24842  dvply2g  24868  elqaalem2  24903  taylfvallem  24940  taylf  24943  tayl0  24944  taylpfval  24947  taylthlem1  24955  taylthlem2  24956  ulmcau  24977  ulmss  24979  ulmdvlem3  24984  mtest  24986  mtestbdd  24987  itgulm2  24991  dvradcnv  25003  pserulm  25004  pserdvlem2  25010  abelthlem9  25022  pige3ALT  25099  logtayl  25237  logccv  25240  loglesqrt  25333  leibpi  25514  rlimcnp  25537  rlimcnp2  25538  xrlimcnp  25540  efrlim  25541  dfef2  25542  o1cxp  25546  cxp2lim  25548  amgmlem  25561  lgamgulmlem2  25601  lgamgulmlem6  25605  lgamcvg2  25626  regamcl  25632  relgamcl  25633  basellem2  25653  basellem3  25654  sqff1o  25753  fsumvma  25783  dchrelbasd  25809  lgseisenlem3  25947  lgseisenlem4  25948  chpo1ub  26050  dchrisum0lem2a  26087  logsqvma2  26113  pnt2  26183  pnt  26184  incistruhgr  26858  minvecolem1  28645  hoaddcl  29529  homulcl  29530  cofmpt2  30373  fpwrelmap  30463  gsummpt2d  30682  xrge0tsmsd  30687  gsumvsca1  30849  gsumvsca2  30850  fedgmullem1  31020  fedgmullem2  31021  ordtrestNEW  31159  esumf1o  31304  esumadd  31311  esumcst  31317  esumpfinval  31329  esumpcvgval  31332  esumcvg  31340  esumsup  31343  measinb  31475  measdivcst  31478  sitgclg  31595  dstfrvclim1  31730  gsumncl  31805  gsumnunsn  31806  fdvneggt  31866  fdvnegge  31868  itgexpif  31872  logdivsqrle  31916  indispconn  32476  cvxpconn  32484  cvmsss2  32516  cvmliftlem6  32532  cvmliftlem8  32534  mrsubcv  32752  mrsubff  32754  mrsubrn  32755  mrsubccat  32760  elmrsubrn  32762  msubrn  32771  msubff  32772  divcnvlin  32959  faclimlem2  32971  faclim  32973  faclim2  32975  knoppcnlem5  33831  knoppcnlem8  33834  knoppcnlem10  33836  knoppcnlem11  33837  curf  34864  finixpnum  34871  matunitlindflem1  34882  matunitlindflem2  34883  ptrest  34885  poimirlem17  34903  poimirlem20  34906  poimirlem24  34910  poimirlem30  34916  broucube  34920  mblfinlem2  34924  volsupnfl  34931  mbfposadd  34933  itg2addnclem2  34938  itg2gt0cn  34941  ibladdnclem  34942  itgaddnclem1  34944  itgaddnc  34946  iblabsnclem  34949  iblabsnc  34950  iblmulc2nc  34951  itgmulc2nclem1  34952  itgmulc2nclem2  34953  itgmulc2nc  34954  itgabsnc  34955  bddiblnc  34956  itggt0cn  34958  ftc1cnnc  34960  ftc1anclem1  34961  ftc1anclem2  34962  ftc1anclem3  34963  ftc1anclem4  34964  ftc1anclem5  34965  ftc1anclem6  34966  ftc1anclem7  34967  ftc1anclem8  34968  ftc1anc  34969  areacirclem4  34979  upixp  34998  totbndbnd  35061  prdsbnd  35065  cntotbnd  35068  rrnequiv  35107  lsatlss  36126  tendoplcl  37911  tendoicl  37926  cmpfiiin  39287  mzpclall  39317  mzpindd  39336  fphpdo  39407  dnnumch3  39640  kelac1  39656  dfac21  39659  itgpowd  39814  rfovcnvf1od  40343  fsovfd  40351  fsovcnvlem  40352  clsk3nimkb  40383  expgrowth  40660  mptelpm  41425  mapss2  41461  monoord2xrv  41753  expcnfg  41865  clim1fr1  41875  sumnnodd  41904  limsupvaluz2  42012  supcnvlimsup  42014  climliminflimsupd  42075  liminfltlem  42078  cncfmptssg  42146  cncfcompt  42159  cxpcncf2  42176  dvsinax  42190  fperdvper  42196  dvcosax  42204  dvnmptdivc  42216  dvnprodlem2  42225  dvnprodlem3  42226  iblsplit  42244  itgcoscmulx  42247  itgiccshift  42258  itgperiod  42259  itgsbtaddcnst  42260  dirkerf  42376  dirkeritg  42381  hoidmvlelem1  42871  hoidmvlelem5  42875  ovnhoilem1  42877  ovnhoilem2  42878  ovnlecvr2  42886  ovncvr2  42887  hoidifhspf  42894  hspmbllem2  42903  opnvonmbllem2  42909  iccvonmbllem  42954  vonioolem1  42956  vonioolem2  42957  vonicclem1  42959  vonicclem2  42960  smfid  43023  funcringcsetcALTV2lem3  44303  funcringcsetclem3ALTV  44326  gsumlsscl  44425  ply1mulgsum  44438  lincfsuppcl  44462  linccl  44463  lincsum  44478  lincscmcl  44481  lcoss  44485  lincext1  44503  el0ldep  44515  lincresunit1  44526  lincresunit3  44530  lmod1zr  44542  fdivmptf  44595  refdivmptf  44596  aacllem  44896  amgmwlem  44897