Theorem fmpttd 7103

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   ↦ cmpt 5185  ⟶wf 6523

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-pr 5390

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 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-fun 6529  df-fn 6530  df-f 6531

This theorem is used by:  fmpt3d  7104  fliftrel  7304  fsetfocdm  8861  curf  8868  pw2f1olem  9078  mapxpen  9140  fsuppssov1  9354  fsuppmptif  9369  wdom2d  9552  cantnflem1d  9667  cantnflem1  9668  ac5num  10087  acni2  10097  infpwfien  10113  fin23lem39  10400  fin1a2lem12  10461  canthp1lem2  10710  wuncval2  10804  gruf  10868  monoord2  14145  seqf1o  14155  ccatcl  14687  swrdcl  14761  swrdwrdsymb  14780  revcl  14878  revlen  14879  ello1mpt  15656  lo1o12  15668  lo1eq  15703  rlimeq  15704  climmpt2  15708  climrecl  15718  climge0  15719  o1compt  15722  rlimcn1b  15724  rlimdiv  15781  isercoll2  15804  caurcvg2  15813  fsumf1o  15857  sumss  15858  fsumss  15859  fsumcl2lem  15865  fsumadd  15874  isumclim3  15893  isummulc2  15896  fsummulc2  15918  fsumrelem  15942  climfsum  15955  isumshft  15976  divcnv  15990  prodfdiv  16033  fprodf1o  16081  prodss  16082  fprodss  16083  fprodser  16084  fprodcl2lem  16085  fprodmul  16095  fproddiv  16096  fprodn0  16114  iprodclim3  16135  fprodefsum  16229  iserodd  16975  prmreclem2  17057  vdwapf  17112  vdwlem4  17124  ramcl  17169  prmodvdslcmf  17187  prdsplusg  17591  prdsmulr  17592  prdsvsca  17593  mrcflem  17742  mreacs  17794  acsfn  17795  hofcllem  18394  hofcl  18395  yonedalem3a  18410  yonedalem4c  18413  yonedainv  18417  prdspjmhm  18987  pwsco1mhm  18990  pwsco2mhm  18991  gsumz  18994  gsumwspan  19004  smndex1gbas  19060  odf1o1  19748  odf1o2  19749  sylow2blem1  19796  mulgmhm  20003  mulgghm  20004  iscyggen2  20057  cyggenod  20060  iscyg3  20062  gsumzsplit  20103  gsumsplit2  20105  gsumconst  20110  gsummptshft  20112  gsummhm2  20115  gsummptmhm  20116  gsummptf1o  20139  gsum2dlem1  20146  gsum2dlem2  20147  gsum2d  20148  prdsgsum  20157  dprdfeq0  20200  dprdlub  20204  dprdz  20208  dprd2dlem1  20219  dprd2da  20220  srglmhm  20409  srgrmhm  20410  ringlghm  20505  ringrghm  20506  gsumdixp  20510  pwspjmhmmgpd  20519  pwsgprod  20521  lmodvsghm  21160  gsumfsum  21702  regsumfsum  21703  expmhm  21704  expghm  21743  evpmodpmf1o  21864  frlmgsum  22040  frlmsplit2  22041  frlmphl  22049  uvcff  22059  uvcresum  22061  snifpsrbag  22190  psrass1lem  22203  rhmpsrlem1  22210  rhmpsrlem2  22211  psrmulcllem  22215  psrlidm  22231  psrridm  22232  psrcom  22237  resspsrmul  22245  mvrf  22254  mplmon  22306  mplmonmul  22307  mplcoe1  22308  mplcoe5lem  22310  mplcoe5  22311  mplbas2  22313  psrbagsn  22334  evlslem4  22347  evlslem2  22350  evlslem3  22351  evlslem6  22352  evlslem1  22353  evlsval2  22358  evlsval3  22360  evlsvvvallem  22362  evlsvvval  22364  selvvvval  22413  psdcl  22444  psdmplcl  22445  psdmul  22449  psropprmul  22517  coe1mul2  22550  coe1tmmul2  22557  coe1tmmul  22558  ply1coe  22578  gsumsmonply1  22587  gsummoncoe1  22588  mamulid  22718  mamurid  22719  mdetunilem9  22897  mdetuni0  22898  mdetmul  22900  smadiadetlem3lem1  22943  matunitlindflem1  22956  matunitlindflem2  22957  m2cpmfo  23036  pmatcollpw1  23056  pmatcollpw3lem  23063  pmatcollpw3fi1lem2  23067  pm2mpcl  23077  mply1topmatcl  23085  mp2pm2mplem2  23087  mp2pm2mp  23091  pm2mpmhmlem2  23099  cayhamlem4  23168  pptbas  23288  tgrest  23439  resttopon  23441  rest0  23449  restfpw  23459  ordtbaslem  23468  ordtuni  23470  ordtrest  23482  cnpfval  23514  pnrmopn  23623  cncmp  23672  discmp  23678  1stcfb  23725  2ndcomap  23739  dis2ndc  23741  comppfsc  23813  kgencmp  23826  ptpjpre1  23852  ptpjcn  23892  ptcldmpt  23895  ptclsg  23896  dfac14  23899  xkoccn  23900  txcnp  23901  ptcnp  23903  uptx  23906  ptcn  23908  ptrescn  23920  xkoptsub  23935  xkoco1cn  23938  xkoco2cn  23939  cnmpt11  23944  pt1hmeo  24087  fbasrn  24165  trfilss  24170  trfg  24172  rnelfmlem  24233  flfcnp2  24288  fclscmpi  24310  alexsublem  24325  ptcmplem3  24335  symgtgp  24387  subgntr  24388  opnsubg  24389  clsnsg  24391  tgpconncomp  24394  eltsms  24414  haustsms  24417  tsmscls  24419  tsms0  24423  tsmsmhm  24427  tgptsmscls  24431  tsmssplit  24433  tsmsxplem1  24434  tsmsxplem2  24435  prdsdsf  24648  prdsxmetlem  24649  imasdsf1olem  24654  prdsbl  24772  stdbdxmet  24796  met1stc  24802  xrge0gsumle  25115  xrge0tsms  25116  cncfmpt2ss  25199  cnmptre  25210  evth  25242  evth2  25243  tcphcph  25520  rrxmval  25688  minveclem1  25707  minveclem3b  25711  iunmbl  25836  uniioombllem3  25868  ismbfcn2  25921  mbfeqalem1  25924  mbfeqalem2  25925  mbfss  25929  mbfmulc2re  25931  mbfneg  25933  mbfpos  25934  mbfposr  25935  mbfposb  25936  mbfadd  25944  mbfmulc2  25946  mbfsup  25947  mbfinf  25948  mbflimsup  25949  mbflimlem  25950  mbflim  25951  itg1climres  25997  mbfi1fseqlem3  26000  mbfi1fseqlem4  26001  mbfi1flimlem  26005  mbfi1flim  26006  mbfmullem2  26007  mbfmul  26009  itg2const2  26024  itg2seq  26025  itg2monolem1  26033  itg2monolem2  26034  itg2monolem3  26035  itg2mono  26036  itg2gt0  26043  itg2cnlem1  26044  itg2cnlem2  26045  itg2cn  26046  iblss  26087  itgitg1  26091  itgle  26092  itgeqa  26096  itgss3  26097  ibladdlem  26102  itgaddlem1  26105  iblabslem  26110  iblabs  26111  iblabsr  26112  iblmulc2  26113  itgmulc2lem1  26114  bddmulibl  26121  bddiblnc  26124  itggt0  26126  itgcn  26127  ellimc2  26159  limcmpt  26165  limcres  26168  limccnp  26173  limccnp2  26174  limcco  26175  perfdvf  26185  dvcnp2  26202  dvaddbr  26220  dvmulbr  26221  dvcjbr  26231  dvexp  26235  dvrec  26237  dvmptres3  26238  dvmptadd  26242  dvmptmul  26243  dvmptres2  26244  dvmptcmul  26246  dvmptcj  26250  dvmptntr  26253  dvmptco  26254  dvcnvlem  26258  dvef  26262  dvferm1  26267  dvferm2  26269  rolle  26272  dvlipcn  26276  dvle  26289  dvivth  26292  lhop1lem  26295  lhop1  26296  lhop2  26297  lhop  26298  dvfsumle  26303  dvfsumge  26304  dvmptrecl  26306  dvfsumlem2  26309  itgsubstlem  26330  itgpowd  26332  tdeglem4  26340  coe1mul3  26379  elply2  26476  plyf  26478  elplyd  26482  plypf1  26493  coeeq2  26523  coemullem  26531  coe1termlem  26539  dvply2g  26570  elqaalem2  26607  taylfvallem  26649  taylf  26652  tayl0  26653  taylpfval  26656  taylthlem1  26664  taylthlem2  26665  ulmcau  26686  ulmss  26688  ulmdvlem3  26693  mtest  26695  mtestbdd  26696  itgulm2  26700  dvradcnv  26712  pserulm  26713  pserdvlem2  26719  abelthlem9  26731  pige3ALT  26812  logtayl  26952  logccv  26955  loglesqrt  27053  leibpi  27234  rlimcnp  27257  rlimcnp2  27258  xrlimcnp  27260  efrlim  27261  dfef2  27262  o1cxp  27266  cxp2lim  27268  amgmlem  27281  lgamgulmlem2  27321  lgamgulmlem6  27325  lgamcvg2  27346  regamcl  27352  relgamcl  27353  basellem2  27373  basellem3  27374  sqff1o  27473  fsumvma  27504  dchrelbasd  27530  lgseisenlem3  27668  lgseisenlem4  27669  chpo1ub  27771  dchrisum0lem2a  27808  logsqvma2  27834  pnt2  27904  pnt  27905  incistruhgr  29591  minvecolem1  31410  hoaddcl  32294  homulcl  32295  cofmpt2  33162  mptiffisupp  33220  fpwrelmap  33259  gsummpt2d  33544  gsummptfsres  33549  gsummptf1od  33550  gsummptfsf1o  33555  gsumfs2d  33556  gsumzrsum  33560  gsummulsubdishift2  33564  gsummulsubdishift1s  33565  gsummulsubdishift2s  33566  xrge0tsmsd  33568  gsumwrd2dccat  33573  gsumvsca1  33721  gsumvsca2  33722  elrgspnlem1  33737  elrgspnlem2  33738  elrgspnlem3  33739  elrgspnlem4  33740  elrgspn  33741  elrgspnsubrunlem2  33743  elrspunidl  33912  elrspunsn  33913  ressply1evls1  34031  evl1deg2  34043  deg1prod  34049  selvascl  34083  selvply1rhmlem1  34086  extvfvcl  34102  evlextv  34108  mplvrpmga  34111  psrgsum  34114  psrmon  34115  psrmonmul  34116  psrmonprod  34118  esplyfvaln  34140  vietadeg1  34144  fedgmullem1  34195  fedgmullem2  34196  evls1fldgencl  34236  fldextrspunlsplem  34239  fldextrspunlsp  34240  extdgfialglem2  34259  ordtrestNEW  34487  esumf1o  34616  esumadd  34623  esumcst  34629  esumpfinval  34641  esumpcvgval  34644  esumcvg  34652  esumsup  34655  measinb  34788  measdivcst  34791  sitgclg  34909  dstfrvclim1  35045  gsumncl  35107  gsumnunsn  35108  fdvneggt  35164  fdvnegge  35166  itgexpif  35170  logdivsqrle  35214  indispconn  35920  cvxpconn  35928  cvmsss2  35960  cvmliftlem6  35976  cvmliftlem8  35978  mrsubcv  36196  mrsubff  36198  mrsubrn  36199  mrsubccat  36204  elmrsubrn  36206  msubrn  36215  msubff  36216  divcnvlin  36419  faclimlem2  36430  faclim  36432  faclim2  36434  knoppcnlem5  37285  knoppcnlem8  37288  knoppcnlem10  37290  knoppcnlem11  37291  finixpnum  38448  ptrest  38457  poimirlem17  38475  poimirlem20  38478  poimirlem24  38482  poimirlem30  38488  broucube  38492  mblfinlem2  38496  volsupnfl  38503  mbfposadd  38505  itg2addnclem2  38510  itg2gt0cn  38513  ibladdnclem  38514  itgaddnclem1  38516  itgaddnc  38518  iblabsnclem  38521  iblabsnc  38522  iblmulc2nc  38523  itgmulc2nclem1  38524  itgmulc2nclem2  38525  itgmulc2nc  38526  itgabsnc  38527  itggt0cn  38528  ftc1cnnc  38530  ftc1anclem1  38531  ftc1anclem2  38532  ftc1anclem3  38533  ftc1anclem4  38534  ftc1anclem5  38535  ftc1anclem6  38536  ftc1anclem7  38537  ftc1anclem8  38538  ftc1anc  38539  areacirclem4  38549  upixp  38583  totbndbnd  38643  prdsbnd  38647  cntotbnd  38650  rrnequiv  38689  lsatlss  39973  tendoplcl  41758  tendoicl  41773  aks4d1p1p5  43045  aks4d1p9  43058  hashscontpow  43092  sticksstones10  43125  sticksstones17  43133  sticksstones18  43134  unitscyglem1  43165  redvmptabs  43339  fimgmcyc  43520  evlsbagval  43536  evlselv  43539  fsuppind  43540  fsuppssind  43543  mhpind  43544  evlsmhpvvval  43545  mhphflem  43546  cmpfiiin  43646  mzpclall  43676  mzpindd  43695  fphpdo  43762  dnnumch3  43992  kelac1  44008  dfac21  44011  cantnfresb  44269  cantnf2  44270  tfsconcatrev  44293  rfovcnvf1od  44948  fsovfd  44956  fsovcnvlem  44957  clsk3nimkb  44984  mnringmulrcld  45170  expgrowth  45263  mptelpm  46112  mapss2  46140  monoord2xrv  46415  expcnfg  46525  clim1fr1  46535  sumnnodd  46564  limsupvaluz2  46670  supcnvlimsup  46672  climliminflimsupd  46733  liminfltlem  46736  cncfmptssg  46803  cncfcompt  46815  cxpcncf2  46831  dvsinax  46845  fperdvper  46851  dvcosax  46858  dvnmptdivc  46870  dvnprodlem2  46879  dvnprodlem3  46880  iblsplit  46898  itgcoscmulx  46901  itgiccshift  46912  itgperiod  46913  itgsbtaddcnst  46914  dirkerf  47029  dirkeritg  47034  hoidmvlelem1  47527  hoidmvlelem5  47531  ovnhoilem1  47533  ovnhoilem2  47534  ovnlecvr2  47542  ovncvr2  47543  hoidifhspf  47550  hspmbllem2  47559  opnvonmbllem2  47565  iccvonmbllem  47610  vonioolem1  47612  vonioolem2  47613  vonicclem1  47615  vonicclem2  47616  smfid  47684  tmachlem-tpcomp  47870  tmachlem-tpopen  47873  cfsetsnfsetf  48050  funcringcsetcALTV2lem3  49311  funcringcsetclem3ALTV  49334  gsumlsscl  49414  ply1mulgsum  49424  lincfsuppcl  49447  linccl  49448  lincsum  49463  lincscmcl  49466  lcoss  49470  lincext1  49488  el0ldep  49500  lincresunit1  49511  lincresunit3  49515  lmod1zr  49527  fdivmptf  49575  refdivmptf  49576  1arymaptf  49675  aacllem  50861  crosspcld  50881  veronesefvcl  50894  veroquadgsumlem  50905  veroquadmodzerod  50906  amgmwlem  50909