Theorem fmpttd 7139

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147   ↦ cmpt 5189  ⟶wf 6554

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-fun 6560  df-fn 6561  df-f 6562

This theorem is used by:  fmpt3d  7140  fliftrel  7339  fsetfocdm  8911  curf  8918  pw2f1olem  9128  mapxpen  9190  fsuppssov1  9403  fsuppmptif  9418  wdom2d  9601  cantnflem1d  9716  cantnflem1  9717  ac5num  10142  acni2  10152  infpwfien  10168  fin23lem39  10455  fin1a2lem12  10516  canthp1lem2  10765  wuncval2  10859  gruf  10923  monoord2  14203  seqf1o  14213  ccatcl  14746  swrdcl  14821  swrdwrdsymb  14840  revcl  14938  revlen  14939  ello1mpt  15717  lo1o12  15729  lo1eq  15764  rlimeq  15765  climmpt2  15769  climrecl  15779  climge0  15780  o1compt  15783  rlimcn1b  15785  rlimdiv  15842  isercoll2  15865  caurcvg2  15874  fsumf1o  15918  sumss  15919  fsumss  15920  fsumcl2lem  15926  fsumadd  15935  isumclim3  15954  isummulc2  15957  fsummulc2  15979  fsumrelem  16003  climfsum  16016  isumshft  16037  divcnv  16051  prodfdiv  16094  fprodf1o  16142  prodss  16143  fprodss  16144  fprodser  16145  fprodcl2lem  16146  fprodmul  16156  fproddiv  16157  fprodn0  16175  iprodclim3  16196  fprodefsum  16290  iserodd  17042  prmreclem2  17124  vdwapf  17179  vdwlem4  17191  ramcl  17236  prmodvdslcmf  17254  prdsplusg  17658  prdsmulr  17659  prdsvsca  17660  mrcflem  17809  mreacs  17861  acsfn  17862  hofcllem  18461  hofcl  18462  yonedalem3a  18477  yonedalem4c  18480  yonedainv  18484  prdspjmhm  19054  pwsco1mhm  19057  pwsco2mhm  19058  gsumz  19061  gsumwspan  19071  smndex1gbas  19127  odf1o1  19816  odf1o2  19817  sylow2blem1  19864  mulgmhm  20071  mulgghm  20072  iscyggen2  20125  cyggenod  20128  iscyg3  20130  gsumzsplit  20171  gsumsplit2  20173  gsumconst  20178  gsummptshft  20180  gsummhm2  20183  gsummptmhm  20184  gsummptf1o  20207  gsum2dlem1  20214  gsum2dlem2  20215  gsum2d  20216  prdsgsum  20225  dprdfeq0  20268  dprdlub  20272  dprdz  20276  dprd2dlem1  20287  dprd2da  20288  srglmhm  20477  srgrmhm  20478  ringlghm  20573  ringrghm  20574  gsumdixp  20578  pwspjmhmmgpd  20587  pwsgprod  20589  lmodvsghm  21228  gsumfsum  21770  regsumfsum  21771  expmhm  21772  expghm  21811  evpmodpmf1o  21932  frlmgsum  22108  frlmsplit2  22109  frlmphl  22117  uvcff  22127  uvcresum  22129  snifpsrbag  22258  psrass1lem  22271  rhmpsrlem1  22278  rhmpsrlem2  22279  psrmulcllem  22283  psrlidm  22299  psrridm  22300  psrcom  22305  resspsrmul  22313  mvrf  22322  mplmon  22374  mplmonmul  22375  mplcoe1  22376  mplcoe5lem  22378  mplcoe5  22379  mplbas2  22381  psrbagsn  22402  evlslem4  22415  evlslem2  22418  evlslem3  22419  evlslem6  22420  evlslem1  22421  evlsval2  22426  evlsval3  22428  evlsvvvallem  22430  evlsvvval  22432  selvvvval  22481  psdcl  22512  psdmplcl  22513  psdmul  22517  psropprmul  22585  coe1mul2  22618  coe1tmmul2  22625  coe1tmmul  22626  ply1coe  22646  gsumsmonply1  22655  gsummoncoe1  22656  mamulid  22786  mamurid  22787  mdetunilem9  22965  mdetuni0  22966  mdetmul  22968  smadiadetlem3lem1  23011  matunitlindflem1  23024  matunitlindflem2  23025  m2cpmfo  23104  pmatcollpw1  23124  pmatcollpw3lem  23131  pmatcollpw3fi1lem2  23135  pm2mpcl  23145  mply1topmatcl  23153  mp2pm2mplem2  23155  mp2pm2mp  23159  pm2mpmhmlem2  23167  cayhamlem4  23236  pptbas  23356  tgrest  23507  resttopon  23509  rest0  23517  restfpw  23527  ordtbaslem  23536  ordtuni  23538  ordtrest  23550  cnpfval  23582  pnrmopn  23691  cncmp  23740  discmp  23746  1stcfb  23793  2ndcomap  23807  dis2ndc  23809  comppfsc  23881  kgencmp  23894  ptpjpre1  23920  ptpjcn  23960  ptcldmpt  23963  ptclsg  23964  dfac14  23967  xkoccn  23968  txcnp  23969  ptcnp  23971  uptx  23974  ptcn  23976  ptrescn  23988  xkoptsub  24003  xkoco1cn  24006  xkoco2cn  24007  cnmpt11  24012  pt1hmeo  24155  fbasrn  24233  trfilss  24238  trfg  24240  rnelfmlem  24301  flfcnp2  24356  fclscmpi  24378  alexsublem  24393  ptcmplem3  24403  symgtgp  24455  subgntr  24456  opnsubg  24457  clsnsg  24459  tgpconncomp  24462  eltsms  24482  haustsms  24485  tsmscls  24487  tsms0  24491  tsmsmhm  24495  tgptsmscls  24499  tsmssplit  24501  tsmsxplem1  24502  tsmsxplem2  24503  prdsdsf  24716  prdsxmetlem  24717  imasdsf1olem  24722  prdsbl  24840  stdbdxmet  24864  met1stc  24870  xrge0gsumle  25183  xrge0tsms  25184  cncfmpt2ss  25267  cnmptre  25278  evth  25310  evth2  25311  tcphcph  25588  rrxmval  25756  minveclem1  25775  minveclem3b  25779  iunmbl  25904  uniioombllem3  25936  ismbfcn2  25989  mbfeqalem1  25992  mbfeqalem2  25993  mbfss  25997  mbfmulc2re  25999  mbfneg  26001  mbfpos  26002  mbfposr  26003  mbfposb  26004  mbfadd  26012  mbfmulc2  26014  mbfsup  26015  mbfinf  26016  mbflimsup  26017  mbflimlem  26018  mbflim  26019  itg1climres  26065  mbfi1fseqlem3  26068  mbfi1fseqlem4  26069  mbfi1flimlem  26073  mbfi1flim  26074  mbfmullem2  26075  mbfmul  26077  itg2const2  26092  itg2seq  26093  itg2monolem1  26101  itg2monolem2  26102  itg2monolem3  26103  itg2mono  26104  itg2gt0  26111  itg2cnlem1  26112  itg2cnlem2  26113  itg2cn  26114  iblss  26155  itgitg1  26159  itgle  26160  itgeqa  26164  itgss3  26165  ibladdlem  26170  itgaddlem1  26173  iblabslem  26178  iblabs  26179  iblabsr  26180  iblmulc2  26181  itgmulc2lem1  26182  bddmulibl  26189  bddiblnc  26192  itggt0  26194  itgcn  26195  ellimc2  26227  limcmpt  26233  limcres  26236  limccnp  26241  limccnp2  26242  limcco  26243  perfdvf  26253  dvcnp2  26270  dvaddbr  26288  dvmulbr  26289  dvcjbr  26299  dvexp  26303  dvrec  26305  dvmptres3  26306  dvmptadd  26310  dvmptmul  26311  dvmptres2  26312  dvmptcmul  26314  dvmptcj  26318  dvmptntr  26321  dvmptco  26322  dvcnvlem  26326  dvef  26330  dvferm1  26335  dvferm2  26337  rolle  26340  dvlipcn  26344  dvle  26357  dvivth  26360  lhop1lem  26363  lhop1  26364  lhop2  26365  lhop  26366  dvfsumle  26371  dvfsumge  26372  dvmptrecl  26374  dvfsumlem2  26377  itgsubstlem  26398  itgpowd  26400  tdeglem4  26408  coe1mul3  26447  elply2  26544  plyf  26546  elplyd  26550  plypf1  26561  coeeq2  26591  coemullem  26599  coe1termlem  26607  dvply2g  26636  elqaalem2  26673  taylfvallem  26715  taylf  26718  tayl0  26719  taylpfval  26722  taylthlem1  26730  taylthlem2  26731  ulmcau  26752  ulmss  26754  ulmdvlem3  26759  mtest  26761  mtestbdd  26762  itgulm2  26766  dvradcnv  26778  pserulm  26779  pserdvlem2  26785  abelthlem9  26797  pige3ALT  26878  logtayl  27018  logccv  27021  loglesqrt  27119  leibpi  27300  rlimcnp  27323  rlimcnp2  27324  xrlimcnp  27326  efrlim  27327  dfef2  27328  o1cxp  27332  cxp2lim  27334  amgmlem  27347  lgamgulmlem2  27387  lgamgulmlem6  27391  lgamcvg2  27412  regamcl  27418  relgamcl  27419  basellem2  27439  basellem3  27440  sqff1o  27539  fsumvma  27570  dchrelbasd  27596  lgseisenlem3  27734  lgseisenlem4  27735  chpo1ub  27837  dchrisum0lem2a  27874  logsqvma2  27900  pnt2  27970  pnt  27971  incistruhgr  29687  minvecolem1  31506  hoaddcl  32390  homulcl  32391  cofmpt2  33300  mptiffisupp  33357  fpwrelmap  33395  gsummpt2d  33680  gsummptfsres  33685  gsummptf1od  33686  gsummptfsf1o  33691  gsumfs2d  33692  gsumzrsum  33696  gsummulsubdishift2  33700  gsummulsubdishift1s  33701  gsummulsubdishift2s  33702  xrge0tsmsd  33704  gsumwrd2dccat  33709  gsumvsca1  33857  gsumvsca2  33858  elrgspnlem1  33873  elrgspnlem2  33874  elrgspnlem3  33875  elrgspnlem4  33876  elrgspn  33877  elrgspnsubrunlem2  33879  elrspunidl  34048  elrspunsn  34049  ressply1evls1  34167  evl1deg2  34179  deg1prod  34185  selvascl  34219  selvply1rhmlem1  34222  extvfvcl  34238  evlextv  34244  mplvrpmga  34247  psrgsum  34250  psrmon  34251  psrmonmul  34252  psrmonprod  34254  esplyfvaln  34276  vietadeg1  34280  fedgmullem1  34331  fedgmullem2  34332  evls1fldgencl  34372  fldextrspunlsplem  34375  fldextrspunlsp  34376  extdgfialglem2  34395  ordtrestNEW  34623  esumf1o  34752  esumadd  34759  esumcst  34765  esumpfinval  34777  esumpcvgval  34780  esumcvg  34788  esumsup  34791  measinb  34924  measdivcst  34927  sitgclg  35044  dstfrvclim1  35180  gsumncl  35242  gsumnunsn  35243  fdvneggt  35299  fdvnegge  35301  itgexpif  35305  logdivsqrle  35349  indispconn  36166  cvxpconn  36174  cvmsss2  36206  cvmliftlem6  36222  cvmliftlem8  36224  mrsubcv  36442  mrsubff  36444  mrsubrn  36445  mrsubccat  36450  elmrsubrn  36452  msubrn  36461  msubff  36462  divcnvlin  36676  faclimlem2  36687  faclim  36689  faclim2  36691  knoppcnlem5  37541  knoppcnlem8  37544  knoppcnlem10  37546  knoppcnlem11  37547  finixpnum  38720  ptrest  38729  poimirlem17  38747  poimirlem20  38750  poimirlem24  38754  poimirlem30  38760  broucube  38764  mblfinlem2  38768  volsupnfl  38775  mbfposadd  38777  itg2addnclem2  38782  itg2gt0cn  38785  ibladdnclem  38786  itgaddnclem1  38788  itgaddnc  38790  iblabsnclem  38793  iblabsnc  38794  iblmulc2nc  38795  itgmulc2nclem1  38796  itgmulc2nclem2  38797  itgmulc2nc  38798  itgabsnc  38799  itggt0cn  38800  ftc1cnnc  38802  ftc1anclem1  38803  ftc1anclem2  38804  ftc1anclem3  38805  ftc1anclem4  38806  ftc1anclem5  38807  ftc1anclem6  38808  ftc1anclem7  38809  ftc1anclem8  38810  ftc1anc  38811  areacirclem4  38821  upixp  38855  totbndbnd  38915  prdsbnd  38919  cntotbnd  38922  rrnequiv  38961  lsatlss  40245  tendoplcl  42030  tendoicl  42045  aks4d1p1p5  43317  aks4d1p9  43330  hashscontpow  43364  sticksstones10  43397  sticksstones17  43405  sticksstones18  43406  unitscyglem1  43437  redvmptabs  43604  fimgmcyc  43791  evlsbagval  43807  evlselv  43810  fsuppind  43811  fsuppssind  43814  mhpind  43815  evlsmhpvvval  43816  mhphflem  43817  cmpfiiin  43901  mzpclall  43931  mzpindd  43950  fphpdo  44017  dnnumch3  44247  kelac1  44258  dfac21  44261  cantnfresb  44518  cantnf2  44519  tfsconcatrev  44542  rfovcnvf1od  45196  fsovfd  45204  fsovcnvlem  45205  clsk3nimkb  45232  mnringmulrcld  45418  expgrowth  45511  mptelpm  46396  mapss2  46424  monoord2xrv  46698  expcnfg  46808  clim1fr1  46818  sumnnodd  46847  limsupvaluz2  46953  supcnvlimsup  46955  climliminflimsupd  47016  liminfltlem  47019  cncfmptssg  47086  cncfcompt  47098  cxpcncf2  47114  dvsinax  47128  fperdvper  47134  dvcosax  47141  dvnmptdivc  47153  dvnprodlem2  47162  dvnprodlem3  47163  iblsplit  47181  itgcoscmulx  47184  itgiccshift  47195  itgperiod  47196  itgsbtaddcnst  47197  dirkerf  47312  dirkeritg  47317  hoidmvlelem1  47810  hoidmvlelem5  47814  ovnhoilem1  47816  ovnhoilem2  47817  ovnlecvr2  47825  ovncvr2  47826  hoidifhspf  47833  hspmbllem2  47842  opnvonmbllem2  47848  iccvonmbllem  47893  vonioolem1  47895  vonioolem2  47896  vonicclem1  47898  vonicclem2  47899  smfid  47967  tmachlem-tpcomp  48153  tmachlem-tpopen  48156  cfsetsnfsetf  48333  funcringcsetcALTV2lem3  49594  funcringcsetclem3ALTV  49617  gsumlsscl  49697  ply1mulgsum  49707  lincfsuppcl  49730  linccl  49731  lincsum  49746  lincscmcl  49749  lcoss  49753  lincext1  49771  el0ldep  49783  lincresunit1  49794  lincresunit3  49798  lmod1zr  49810  fdivmptf  49858  refdivmptf  49859  1arymaptf  49958  aacllem  51219  crosspcld  51239  veronesefvcl  51252  veroquadgsumlem  51263  veroquadmodzerod  51264  amgmwlem  51267