Theorem fmpttd 7110

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2142   ↦ cmpt 5191  ⟶wf 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-fun 6538  df-fn 6539  df-f 6540

This theorem is used by:  fmpt3d  7111  fliftrel  7306  fsetfocdm  8856  pw2f1olem  9067  mapxpen  9129  fsuppssov1  9342  fsuppmptif  9357  wdom2d  9540  cantnflem1d  9655  cantnflem1  9656  ac5num  10027  acni2  10037  infpwfien  10053  fin23lem39  10340  fin1a2lem12  10401  canthp1lem2  10644  wuncval2  10738  gruf  10802  monoord2  14076  seqf1o  14086  ccatcl  14618  swrdcl  14690  swrdwrdsymb  14707  revcl  14805  revlen  14806  ello1mpt  15579  lo1o12  15591  lo1eq  15626  rlimeq  15627  climmpt2  15631  climrecl  15641  climge0  15642  o1compt  15645  rlimcn1b  15647  rlimdiv  15704  isercoll2  15727  caurcvg2  15736  fsumf1o  15781  sumss  15782  fsumss  15783  fsumcl2lem  15789  fsumadd  15798  isumclim3  15817  isummulc2  15820  fsummulc2  15842  fsumrelem  15866  climfsum  15879  isumshft  15900  divcnv  15914  prodfdiv  15957  fprodf1o  16007  prodss  16008  fprodss  16009  fprodser  16010  fprodcl2lem  16011  fprodmul  16021  fproddiv  16022  fprodn0  16040  iprodclim3  16061  fprodefsum  16155  iserodd  16901  prmreclem2  16983  vdwapf  17038  vdwlem4  17050  ramcl  17095  prmodvdslcmf  17113  prdsplusg  17517  prdsmulr  17518  prdsvsca  17519  mrcflem  17668  mreacs  17720  acsfn  17721  hofcllem  18320  hofcl  18321  yonedalem3a  18336  yonedalem4c  18339  yonedainv  18343  prdspjmhm  18894  pwsco1mhm  18897  pwsco2mhm  18898  gsumz  18901  gsumwspan  18911  smndex1gbas  18967  odf1o1  19648  odf1o2  19649  sylow2blem1  19696  mulgmhm  19903  mulgghm  19904  iscyggen2  19957  cyggenod  19960  iscyg3  19962  gsumzsplit  20003  gsumsplit2  20005  gsumconst  20010  gsummptshft  20012  gsummhm2  20015  gsummptmhm  20016  gsummptf1o  20039  gsum2dlem1  20046  gsum2dlem2  20047  gsum2d  20048  prdsgsum  20057  dprdfeq0  20100  dprdlub  20104  dprdz  20108  dprd2dlem1  20119  dprd2da  20120  srglmhm  20309  srgrmhm  20310  ringlghm  20402  ringrghm  20403  gsumdixp  20407  pwspjmhmmgpd  20416  pwsgprod  20418  lmodvsghm  21055  gsumfsum  21595  regsumfsum  21596  expmhm  21597  expghm  21636  evpmodpmf1o  21757  frlmgsum  21933  frlmsplit2  21934  frlmphl  21942  uvcff  21952  uvcresum  21954  snifpsrbag  22081  psrass1lem  22094  rhmpsrlem1  22101  rhmpsrlem2  22102  psrmulcllem  22106  psrlidm  22122  psrridm  22123  psrcom  22128  resspsrmul  22136  mvrf  22145  mplmon  22197  mplmonmul  22198  mplcoe1  22199  mplcoe5lem  22201  mplcoe5  22202  mplbas2  22204  psrbagsn  22225  evlslem4  22238  evlslem2  22241  evlslem3  22242  evlslem6  22243  evlslem1  22244  evlsval2  22249  evlsval3  22251  evlsvvvallem  22253  evlsvvval  22255  selvvvval  22304  psdcl  22335  psdmplcl  22336  psdmul  22340  psropprmul  22408  coe1mul2  22441  coe1tmmul2  22448  coe1tmmul  22449  ply1coe  22469  gsumsmonply1  22478  gsummoncoe1  22479  mamulid  22609  mamurid  22610  mdetunilem9  22788  mdetuni0  22789  mdetmul  22791  smadiadetlem3lem1  22834  m2cpmfo  22924  pmatcollpw1  22944  pmatcollpw3lem  22951  pmatcollpw3fi1lem2  22955  pm2mpcl  22965  mply1topmatcl  22973  mp2pm2mplem2  22975  mp2pm2mp  22979  pm2mpmhmlem2  22987  cayhamlem4  23056  pptbas  23176  tgrest  23327  resttopon  23329  rest0  23337  restfpw  23347  ordtbaslem  23356  ordtuni  23358  ordtrest  23370  cnpfval  23402  pnrmopn  23511  cncmp  23560  discmp  23566  1stcfb  23613  2ndcomap  23626  dis2ndc  23628  comppfsc  23700  kgencmp  23713  ptpjpre1  23739  ptpjcn  23779  ptcldmpt  23782  ptclsg  23783  dfac14  23786  xkoccn  23787  txcnp  23788  ptcnp  23790  uptx  23793  ptcn  23795  ptrescn  23807  xkoptsub  23822  xkoco1cn  23825  xkoco2cn  23826  cnmpt11  23831  pt1hmeo  23974  fbasrn  24052  trfilss  24057  trfg  24059  rnelfmlem  24120  flfcnp2  24175  fclscmpi  24197  alexsublem  24212  ptcmplem3  24222  symgtgp  24274  subgntr  24275  opnsubg  24276  clsnsg  24278  tgpconncomp  24281  eltsms  24301  haustsms  24304  tsmscls  24306  tsms0  24310  tsmsmhm  24314  tgptsmscls  24318  tsmssplit  24320  tsmsxplem1  24321  tsmsxplem2  24322  prdsdsf  24535  prdsxmetlem  24536  imasdsf1olem  24541  prdsbl  24659  stdbdxmet  24683  met1stc  24689  xrge0gsumle  25002  xrge0tsms  25003  cncfmpt2ss  25086  cnmptre  25097  evth  25129  evth2  25130  tcphcph  25407  rrxmval  25575  minveclem1  25594  minveclem3b  25598  iunmbl  25723  uniioombllem3  25755  ismbfcn2  25808  mbfeqalem1  25811  mbfeqalem2  25812  mbfss  25816  mbfmulc2re  25818  mbfneg  25820  mbfpos  25821  mbfposr  25822  mbfposb  25823  mbfadd  25831  mbfmulc2  25833  mbfsup  25834  mbfinf  25835  mbflimsup  25836  mbflimlem  25837  mbflim  25838  itg1climres  25884  mbfi1fseqlem3  25887  mbfi1fseqlem4  25888  mbfi1flimlem  25892  mbfi1flim  25893  mbfmullem2  25894  mbfmul  25896  itg2const2  25911  itg2seq  25912  itg2monolem1  25920  itg2monolem2  25921  itg2monolem3  25922  itg2mono  25923  itg2gt0  25930  itg2cnlem1  25931  itg2cnlem2  25932  itg2cn  25933  iblss  25975  itgitg1  25979  itgle  25980  itgeqa  25984  itgss3  25985  ibladdlem  25990  itgaddlem1  25993  iblabslem  25998  iblabs  25999  iblabsr  26000  iblmulc2  26001  itgmulc2lem1  26002  bddmulibl  26009  bddiblnc  26012  itggt0  26014  itgcn  26015  ellimc2  26047  limcmpt  26053  limcres  26056  limccnp  26061  limccnp2  26062  limcco  26063  perfdvf  26073  dvcnp2  26090  dvaddbr  26108  dvmulbr  26109  dvcjbr  26119  dvexp  26123  dvrec  26125  dvmptres3  26126  dvmptadd  26130  dvmptmul  26131  dvmptres2  26132  dvmptcmul  26134  dvmptcj  26138  dvmptntr  26141  dvmptco  26142  dvcnvlem  26146  dvef  26150  dvferm1  26155  dvferm2  26157  rolle  26160  dvlipcn  26164  dvle  26177  dvivth  26180  lhop1lem  26183  lhop1  26184  lhop2  26185  lhop  26186  dvfsumle  26191  dvfsumge  26192  dvmptrecl  26194  dvfsumlem2  26197  itgsubstlem  26218  itgpowd  26220  tdeglem4  26228  coe1mul3  26267  elply2  26364  plyf  26366  elplyd  26370  plypf1  26380  coeeq2  26410  coemullem  26418  coe1termlem  26426  dvply2g  26457  elqaalem2  26492  taylfvallem  26532  taylf  26535  tayl0  26536  taylpfval  26539  taylthlem1  26547  taylthlem2  26548  ulmcau  26569  ulmss  26571  ulmdvlem3  26576  mtest  26578  mtestbdd  26579  itgulm2  26583  dvradcnv  26595  pserulm  26596  pserdvlem2  26602  abelthlem9  26614  pige3ALT  26696  logtayl  26836  logccv  26839  loglesqrt  26937  leibpi  27118  rlimcnp  27141  rlimcnp2  27142  xrlimcnp  27144  efrlim  27145  dfef2  27146  o1cxp  27150  cxp2lim  27152  amgmlem  27165  lgamgulmlem2  27205  lgamgulmlem6  27209  lgamcvg2  27230  regamcl  27236  relgamcl  27237  basellem2  27257  basellem3  27258  sqff1o  27357  fsumvma  27388  dchrelbasd  27414  lgseisenlem3  27552  lgseisenlem4  27553  chpo1ub  27655  dchrisum0lem2a  27692  logsqvma2  27718  pnt2  27788  pnt  27789  incistruhgr  29440  minvecolem1  31237  hoaddcl  32121  homulcl  32122  cofmpt2  32990  mptiffisupp  33049  fpwrelmap  33089  gsummpt2d  33378  gsummptfsres  33383  gsummptf1od  33384  gsummptfsf1o  33389  gsumfs2d  33390  gsumzrsum  33394  gsummulsubdishift2  33398  gsummulsubdishift1s  33399  gsummulsubdishift2s  33400  xrge0tsmsd  33402  gsumwrd2dccat  33407  gsumvsca1  33555  gsumvsca2  33556  elrgspnlem1  33571  elrgspnlem2  33572  elrgspnlem3  33573  elrgspnlem4  33574  elrgspn  33575  elrgspnsubrunlem2  33577  elrspunidl  33745  elrspunsn  33746  ressply1evls1  33864  evl1deg2  33876  deg1prod  33882  selvascl  33916  selvply1rhmlem1  33919  extvfvcl  33935  evlextv  33941  mplvrpmga  33944  psrgsum  33947  psrmon  33948  psrmonmul  33949  psrmonprod  33951  esplyfvaln  33973  vietadeg1  33977  fedgmullem1  34028  fedgmullem2  34029  evls1fldgencl  34069  fldextrspunlsplem  34072  fldextrspunlsp  34073  extdgfialglem2  34092  ordtrestNEW  34320  esumf1o  34449  esumadd  34456  esumcst  34462  esumpfinval  34474  esumpcvgval  34477  esumcvg  34485  esumsup  34488  measinb  34620  measdivcst  34623  sitgclg  34741  dstfrvclim1  34877  gsumncl  34939  gsumnunsn  34940  fdvneggt  34996  fdvnegge  34998  itgexpif  35002  logdivsqrle  35046  indispconn  35734  cvxpconn  35742  cvmsss2  35774  cvmliftlem6  35790  cvmliftlem8  35792  mrsubcv  36010  mrsubff  36012  mrsubrn  36013  mrsubccat  36018  elmrsubrn  36020  msubrn  36029  msubff  36030  divcnvlin  36233  faclimlem2  36244  faclim  36246  faclim2  36248  knoppcnlem5  37114  knoppcnlem8  37117  knoppcnlem10  37119  knoppcnlem11  37120  curf  38277  finixpnum  38284  matunitlindflem1  38295  matunitlindflem2  38296  ptrest  38298  poimirlem17  38316  poimirlem20  38319  poimirlem24  38323  poimirlem30  38329  broucube  38333  mblfinlem2  38337  volsupnfl  38344  mbfposadd  38346  itg2addnclem2  38351  itg2gt0cn  38354  ibladdnclem  38355  itgaddnclem1  38357  itgaddnc  38359  iblabsnclem  38362  iblabsnc  38363  iblmulc2nc  38364  itgmulc2nclem1  38365  itgmulc2nclem2  38366  itgmulc2nc  38367  itgabsnc  38368  itggt0cn  38369  ftc1cnnc  38371  ftc1anclem1  38372  ftc1anclem2  38373  ftc1anclem3  38374  ftc1anclem4  38375  ftc1anclem5  38376  ftc1anclem6  38377  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  areacirclem4  38390  upixp  38408  totbndbnd  38468  prdsbnd  38472  cntotbnd  38475  rrnequiv  38514  lsatlss  39798  tendoplcl  41583  tendoicl  41598  aks4d1p1p5  42870  aks4d1p9  42883  hashscontpow  42917  sticksstones10  42950  sticksstones17  42958  sticksstones18  42959  unitscyglem1  42990  redvmptabs  43149  fimgmcyc  43330  evlsbagval  43346  evlselv  43349  fsuppind  43350  fsuppssind  43353  mhpind  43354  evlsmhpvvval  43355  mhphflem  43356  cmpfiiin  43456  mzpclall  43486  mzpindd  43505  fphpdo  43572  dnnumch3  43802  kelac1  43818  dfac21  43821  cantnfresb  44079  cantnf2  44080  tfsconcatrev  44103  rfovcnvf1od  44758  fsovfd  44766  fsovcnvlem  44767  clsk3nimkb  44794  mnringmulrcld  44980  expgrowth  45073  mptelpm  45922  mapss2  45950  monoord2xrv  46225  expcnfg  46335  clim1fr1  46345  sumnnodd  46374  limsupvaluz2  46480  supcnvlimsup  46482  climliminflimsupd  46543  liminfltlem  46546  cncfmptssg  46613  cncfcompt  46625  cxpcncf2  46641  dvsinax  46655  fperdvper  46661  dvcosax  46668  dvnmptdivc  46680  dvnprodlem2  46689  dvnprodlem3  46690  iblsplit  46708  itgcoscmulx  46711  itgiccshift  46722  itgperiod  46723  itgsbtaddcnst  46724  dirkerf  46839  dirkeritg  46844  hoidmvlelem1  47337  hoidmvlelem5  47341  ovnhoilem1  47343  ovnhoilem2  47344  ovnlecvr2  47352  ovncvr2  47353  hoidifhspf  47360  hspmbllem2  47369  opnvonmbllem2  47375  iccvonmbllem  47420  vonioolem1  47422  vonioolem2  47423  vonicclem1  47425  vonicclem2  47426  smfid  47494  cfsetsnfsetf  47823  funcringcsetcALTV2lem3  49085  funcringcsetclem3ALTV  49108  gsumlsscl  49188  ply1mulgsum  49198  lincfsuppcl  49221  linccl  49222  lincsum  49237  lincscmcl  49240  lcoss  49244  lincext1  49262  el0ldep  49274  lincresunit1  49285  lincresunit3  49289  lmod1zr  49301  fdivmptf  49349  refdivmptf  49350  1arymaptf  49449  aacllem  50649  crosspcli  50668  amgmwlem  50677