Theorem fmptd 6292

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.)

Hypotheses

Ref	Expression
fmptd.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
fmptd.2	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
fmptd	⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜑,𝑥

Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem fmptd

Step	Hyp	Ref	Expression
1		fmptd.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
2	1	ralrimiva 2949	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶)
3		fmptd.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	fmpt 6289	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹:𝐴⟶𝐶)
5	2, 4	sylib 207	1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896   ↦ cmpt 4643  ⟶wf 5800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812

This theorem is referenced by:  fmpt3d  6293  fliftrel  6458  off  6810  caofinvl  6822  curry1f  7158  curry2f  7160  fnwelem  7179  fdiagfn  7787  resixpfo  7832  pw2f1olem  7949  mapxpen  8011  xpmapenlem  8012  unxpdomlem3  8051  fsuppmptdm  8169  fsuppmptif  8188  wdom2d  8368  cantnfp1lem1  8458  cantnfp1lem2  8459  cantnfp1lem3  8460  cantnflem1d  8468  cantnflem1  8469  cantnf  8473  fseqenlem1  8730  fseqenlem2  8731  dfac8clem  8738  ac5num  8742  acni2  8752  infpwfien  8768  coftr  8978  fin23lem39  9055  isf34lem2  9078  fin1a2lem12  9116  axcc2lem  9141  axdc2lem  9153  axdc3lem4  9158  pwcfsdom  9284  canthp1lem2  9354  wuncval2  9448  gruf  9512  rpnnen1lem1  11691  rpnnen1lem1OLD  11697  monoord2  12694  seqf1o  12704  ccatcl  13212  swrdcl  13271  revcl  13361  revlen  13362  ello1mpt  14100  lo1o12  14112  lo1eq  14147  rlimeq  14148  climmpt2  14152  climrecl  14162  climge0  14163  o1compt  14166  rlimcn1b  14168  rlimdiv  14224  isercoll2  14247  caurcvg2  14256  caucvg  14257  sumrblem  14289  summolem2a  14293  fsumf1o  14301  sumss  14302  fsumss  14303  fsumcl2lem  14309  fsumadd  14317  isumclim3  14332  isummulc2  14335  fsummulc2  14358  fsumrelem  14380  climfsum  14393  isumshft  14410  divcnv  14424  supcvg  14427  prodfdiv  14467  prodrblem  14498  prodmolem2a  14503  fprodf1o  14515  prodss  14516  fprodss  14517  fprodser  14518  fprodcl2lem  14519  fprodmul  14529  fproddiv  14530  fprodn0  14548  iprodclim3  14570  fprodefsum  14664  rpnnen2lem2  14783  crth  15321  eulerthlem1  15324  iserodd  15378  prmreclem2  15459  prmreclem6  15463  1arithlem3  15467  4sqlem11  15497  vdwapf  15514  vdwlem2  15524  vdwlem4  15526  vdwlem6  15528  vdwlem10  15532  ramub1lem2  15569  ramcl  15571  prmodvdslcmf  15589  prmgaplcm  15602  prdsplusg  15941  prdsmulr  15942  prdsvsca  15943  mrcflem  16089  mreacs  16142  acsfn  16143  homaf  16503  funcestrcsetclem3  16605  funcsetcestrclem3  16619  prfcl  16666  curf1cl  16691  hofcllem  16721  hofcl  16722  yonedalem3a  16737  yonedalem4c  16740  yonedainv  16744  prdspjmhm  17190  pwsco1mhm  17193  pwsco2mhm  17194  gsumz  17197  gsumwspan  17206  vrmdfval  17216  vrmdf  17218  frmdup1  17224  grpinvf  17289  cycsubgcl  17443  cycsubgss  17444  conjghm  17514  conjnmz  17517  qusghm  17520  galactghm  17646  symgextf  17660  symgfixf  17679  pmtrf  17698  pmtrdifwrdellem1  17724  psgnunilem5  17737  odf1  17802  dfod2  17804  odf1o2  17811  pgpssslw  17852  sylow2blem1  17858  pj1f  17933  frgpmhm  18001  vrgpf  18004  mulgmhm  18056  mulgghm  18057  iscyggen2  18106  cyggenod  18109  iscyg3  18111  gsummptfsadd  18147  gsumzsplit  18150  gsumsplit2  18152  gsummptfidmsplitres  18154  gsumconst  18157  gsummptshft  18159  gsummhm2  18162  gsummptmhm  18163  gsummptfidminv  18170  gsummptfssub  18172  gsumzunsnd  18178  gsummptf1o  18185  gsummpt1n0  18187  gsum2dlem1  18192  gsum2dlem2  18193  gsum2d  18194  prdsgsum  18200  dprdfeq0  18244  dprdlub  18248  dprdz  18252  dprd2dlem1  18263  dprd2da  18264  ablfac1b  18292  ablfac2  18311  srglmhm  18358  srgrmhm  18359  ringlghm  18427  ringrghm  18428  gsumdixp  18432  abvtrivd  18663  issrngd  18684  lmodvsghm  18747  lspf  18795  pwssplit0  18879  asclf  19158  snifpsrbag  19187  psrass1lem  19198  psrmulcllem  19208  psr1cl  19223  psrlidm  19224  psrridm  19225  psrcom  19230  resspsrmul  19238  subrgpsr  19240  mvrf  19245  mplmon  19284  mplmonmul  19285  mplcoe1  19286  mplcoe5lem  19288  mplcoe5  19289  mplbas2  19291  psrbagsn  19316  evlslem4  19329  evlslem2  19333  evlslem6  19334  evlslem3  19335  evlslem1  19336  evlsval2  19341  psropprmul  19429  coe1mul2  19460  coe1tmmul2  19467  coe1tmmul  19468  ply1coe  19487  gsumsmonply1  19494  gsummoncoe1  19495  gsumfsum  19632  regsumfsum  19633  expmhm  19634  expghm  19663  mulgghm2  19664  evpmodpmf1o  19761  isphld  19818  pjff  19875  frlmgsum  19930  frlmsplit2  19931  frlmphl  19939  uvcff  19949  uvcresum  19951  frlmup1  19956  mamulid  20066  mamurid  20067  scmatf  20154  mdetf  20220  mdetunilem9  20245  mdetuni0  20246  mdetmul  20248  maduf  20266  smadiadetlem3lem1  20291  cpm2mf  20376  m2cpmfo  20380  pmatcollpw1  20400  pmatcollpw3lem  20407  pmatcollpw3fi1lem1  20410  pmatcollpw3fi1lem2  20411  pm2mpcl  20421  mply1topmatcl  20429  mp2pm2mplem2  20431  mp2pm2mp  20435  pm2mpmhmlem2  20443  chfacfisf  20478  chfacfisfcpmat  20479  cpmidpmatlem2  20495  cayhamlem4  20512  pptbas  20622  tgrest  20773  resttopon  20775  rest0  20783  restfpw  20793  ordtbaslem  20802  ordtuni  20804  ordtrest  20816  cnpfval  20848  pnrmopn  20957  cncmp  21005  discmp  21011  1stcfb  21058  2ndcomap  21071  dis2ndc  21073  lly1stc  21109  comppfsc  21145  kgencmp  21158  ptpjpre1  21184  ptpjcn  21224  ptcldmpt  21227  ptclsg  21228  dfac14  21231  xkoccn  21232  txcnp  21233  ptcnp  21235  txcnmpt  21237  uptx  21238  ptcn  21240  ptrescn  21252  txlm  21261  xkoptsub  21267  xkoco1cn  21270  xkoco2cn  21271  cnmpt11  21276  xkoinjcn  21300  kqffn  21338  pt1hmeo  21419  fbasrn  21498  trfilss  21503  trfg  21505  rnelfmlem  21566  txflf  21620  flfcnp2  21621  fclscmpi  21643  alexsublem  21658  ptcmplem3  21668  symgtgp  21715  subgntr  21720  opnsubg  21721  clsnsg  21723  tgpconcomp  21726  tsmsfbas  21741  eltsms  21746  haustsms  21749  tsmscls  21751  tsms0  21755  tsmsmhm  21759  tgptsmscls  21763  tsmssplit  21765  tsmsxplem1  21766  tsmsxplem2  21767  ustuqtop0  21854  prdsdsf  21982  prdsxmetlem  21983  imasdsf1olem  21988  prdsbl  22106  stdbdxmet  22130  met1stc  22136  nmf2  22207  xrge0gsumle  22444  xrge0tsms  22445  metdsf  22459  metdsge  22460  mulc1cncf  22516  cncfmpt2ss  22526  cnmptre  22534  evth  22566  evth2  22567  lebnumlem1  22568  cphnmf  22803  tchcph  22844  cmetcaulem  22894  rrxmval  22996  minveclem1  23003  minveclem3b  23007  ovollb2lem  23063  ovolctb  23065  ovolunlem1a  23071  ovolunlem1  23072  ovoliunlem1  23077  ovoliunlem2  23078  ovoliun  23080  ovolshftlem1  23084  ovolscalem1  23088  ovolicc1  23091  iunmbl  23128  ioombl1lem1  23133  uniioombllem2  23157  uniioombllem3  23159  volsup2  23179  volcn  23180  vitalilem4  23186  vitalilem5  23187  mbfconst  23208  ismbfcn2  23212  mbfeqalem  23215  mbfss  23219  mbfmulc2re  23221  mbfmax  23222  mbfneg  23223  mbfpos  23224  mbfposr  23225  mbfposb  23226  mbfadd  23234  mbfmulc2  23236  mbfsup  23237  mbfinf  23238  mbflimsup  23239  mbflimlem  23240  mbflim  23241  i1f1lem  23262  i1f1  23263  i1fres  23278  itg1climres  23287  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  mbfi1flimlem  23295  mbfi1flim  23296  mbfmullem2  23297  mbfmul  23299  itg2const2  23314  itg2seq  23315  itg2splitlem  23321  itg2split  23322  itg2monolem1  23323  itg2monolem2  23324  itg2monolem3  23325  itg2mono  23326  itg2i1fseq  23328  itg2i1fseq2  23329  itg2gt0  23333  itg2cnlem1  23334  itg2cnlem2  23335  itg2cn  23336  iblss  23377  itgitg1  23381  itgle  23382  itgeqa  23386  itgss3  23387  ibladdlem  23392  itgaddlem1  23395  iblabslem  23400  iblabs  23401  iblabsr  23402  iblmulc2  23403  itgmulc2lem1  23404  bddmulibl  23411  itggt0  23414  itgcn  23415  ellimc2  23447  limcmpt  23453  limcres  23456  limccnp  23461  limccnp2  23462  limcco  23463  perfdvf  23473  dvreslem  23479  dvcnp2  23489  dvaddbr  23507  dvmulbr  23508  dvcjbr  23518  dvexp  23522  dvrec  23524  dvmptres3  23525  dvmptadd  23529  dvmptmul  23530  dvmptres2  23531  dvmptcmul  23533  dvmptcj  23537  dvmptntr  23540  dvmptco  23541  dvcnvlem  23543  dvef  23547  dvferm1  23552  dvferm2  23554  rolle  23557  dvlipcn  23561  dvle  23574  dvivthlem1  23575  dvivth  23577  lhop1lem  23580  lhop1  23581  lhop2  23582  lhop  23583  dvfsumle  23588  dvfsumge  23589  dvmptrecl  23591  dvfsumrlimf  23592  dvfsumlem2  23594  dvfsumlem3  23595  ftc1lem2  23603  ftc1lem6  23608  itgsubstlem  23615  tdeglem1  23622  tdeglem4  23624  coe1mul3  23663  elply2  23756  plyf  23758  elplyd  23762  plypf1  23772  coeeq2  23802  coemullem  23810  coe1termlem  23818  dvply2g  23844  elqaalem2  23879  taylfvallem  23916  taylf  23919  tayl0  23920  taylpfval  23923  taylpf  23924  taylthlem1  23931  taylthlem2  23932  ulmshftlem  23947  ulmshft  23948  ulmcau  23953  ulmss  23955  ulmdvlem1  23958  ulmdvlem3  23960  mtest  23962  mtestbdd  23963  itgulm2  23967  psergf  23970  radcnvlem1  23971  dvradcnv  23979  pserulm  23980  psercn2  23981  pserdvlem2  23986  abelthlem4  23992  abelthlem9  23998  pige3  24073  efif1olem4  24095  logtayl  24206  logccv  24209  loglesqrt  24299  logbf  24327  leibpi  24469  rlimcnp  24492  rlimcnp2  24493  xrlimcnp  24495  efrlim  24496  dfef2  24497  o1cxp  24501  cxp2lim  24503  amgmlem  24516  lgamgulmlem2  24556  lgamgulmlem6  24560  lgamcvg2  24581  gamcvg  24582  regamcl  24587  relgamcl  24588  basellem2  24608  basellem4  24610  basellem7  24613  basellem9  24615  sqff1o  24708  fsumvma  24738  dchrelbasd  24764  lgsfcl2  24828  lgsqrlem2  24872  lgseisenlem1  24900  lgseisenlem3  24902  lgseisenlem4  24903  chpo1ub  24969  dchrmusum2  24983  dchrvmasumiflem1  24990  dchrisum0ff  24996  dchrisum0lem1b  25004  dchrisum0lem2a  25006  logsqvma2  25032  pnt2  25102  pnt  25103  abvcxp  25104  padicabv  25119  lmif  25477  axlowdimlem15  25636  incistruhgr  25746  nbgraf1olem2  25971  wlkiswwlk2lem5  26223  wlknwwlknfun  26238  wlkiswwlkfun  26245  wwlkextfun  26257  clwlkisclwwlklem2a  26313  clwwlkf  26322  clwlkfclwwlk  26371  vdgrf  26425  vdgrfif  26426  frgrancvvdeqlem5  26561  numclwlk1lem2f  26619  numclwlk2lem2f  26630  ipblnfi  27095  ubthlem1  27110  minvecolem1  27114  htthlem  27158  hlimadd  27434  chscllem1  27880  hoaddcl  28001  homulcl  28002  brafn  28190  kbop  28196  cnlnadjlem2  28311  strlem3a  28495  hstrlem3a  28503  off2  28823  xppreima2  28830  fpwrelmap  28896  gsummpt2d  29112  gsumvsca1  29113  gsumvsca2  29114  xrge0tsmsd  29116  ordtrestNEW  29295  xrge0mulc1cn  29315  esumf1o  29439  esumadd  29446  esumcst  29452  esumpfinval  29464  esumpcvgval  29467  esumcvg  29475  esumsup  29478  measinb  29611  measdivcst  29615  mbfmco2  29654  sitgclg  29731  eulerpartlems  29749  dstfrvclim1  29866  gsumncl  29941  gsumnunsn  29942  erdszelem9  30435  indispcon  30470  cvxpcon  30478  cvmsss2  30510  cvmliftlem6  30526  cvmliftlem8  30528  cvmlift3lem3  30557  mrsubcv  30661  mrsubff  30663  mrsubrn  30664  mrsubccat  30669  elmrsubrn  30671  msubrn  30680  msubff  30681  mvhf  30709  divcnvlin  30871  iprodefisum  30880  faclimlem2  30883  faclim  30885  faclim2  30887  knoppcnlem5  31657  knoppcnlem8  31660  knoppcnlem10  31662  knoppcnlem11  31663  unbdqndv1  31669  knoppf  31696  curf  32557  finixpnum  32564  matunitlindflem1  32575  matunitlindflem2  32576  ptrest  32578  poimirlem17  32596  poimirlem20  32599  poimirlem24  32603  poimirlem30  32609  broucube  32613  mblfinlem2  32617  volsupnfl  32624  mbfposadd  32627  itg2addnclem2  32632  itg2gt0cn  32635  ibladdnclem  32636  itgaddnclem1  32638  itgaddnc  32640  iblabsnclem  32643  iblabsnc  32644  iblmulc2nc  32645  itgmulc2nclem1  32646  itgmulc2nclem2  32647  itgmulc2nc  32648  itgabsnc  32649  bddiblnc  32650  itggt0cn  32652  ftc1cnnc  32654  ftc1anclem1  32655  ftc1anclem2  32656  ftc1anclem3  32657  ftc1anclem4  32658  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  areacirclem4  32673  upixp  32694  totbndbnd  32758  prdsbnd  32762  cntotbnd  32765  rrnequiv  32804  lsatlss  33301  lflnegcl  33380  lshpkrcl  33421  tendoplcl  35087  tendo0cl  35096  tendoicl  35102  cmpfiiin  36278  mzpclall  36308  mzpindd  36327  fphpdo  36399  dnnumch3  36635  kelac1  36651  dfac21  36654  itgpowd  36819  rfovcnvf1od  37318  fsovfd  37326  fsovcnvlem  37327  clsk3nimkb  37358  expgrowth  37556  binomcxplemradcnv  37573  binomcxplemcvg  37575  binomcxplemnotnn0  37577  rnmptc  38348  mptelpm  38352  projf1o  38381  mapss2  38392  expcnfg  38658  clim1fr1  38668  mullimc  38683  ellimcabssub0  38684  mullimcf  38690  constlimc  38691  idlimc  38693  sumnnodd  38697  neglimc  38714  addlimc  38715  0ellimcdiv  38716  fnlimf  38745  cncfmptssg  38755  cncfshift  38759  cncfcompt  38768  icccncfext  38773  cncfiooiccre  38781  cxpcncf2  38786  fprodsubrecnncnvlem  38794  fprodaddrecnncnvlem  38796  dvsinax  38801  fperdvper  38808  dvmptresicc  38809  dvcosax  38816  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnmptdivc  38828  dvnxpaek  38832  dvnprodlem1  38836  dvnprodlem2  38837  dvnprodlem3  38838  itgsinexplem1  38845  iblsplit  38858  itgcoscmulx  38861  itgiccshift  38872  itgperiod  38873  itgsbtaddcnst  38874  dirkerf  38990  dirkeritg  38995  dirkercncflem2  38997  fourierdlem4  39004  fourierdlem5  39005  fourierdlem9  39009  fourierdlem14  39014  fourierdlem16  39016  fourierdlem17  39017  fourierdlem18  39018  fourierdlem21  39021  fourierdlem22  39022  fourierdlem37  39037  fourierdlem50  39049  fourierdlem51  39050  fourierdlem53  39052  fourierdlem55  39054  fourierdlem57  39056  fourierdlem58  39057  fourierdlem59  39058  fourierdlem60  39059  fourierdlem61  39060  fourierdlem67  39066  fourierdlem68  39067  fourierdlem72  39071  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem78  39077  fourierdlem80  39079  fourierdlem81  39080  fourierdlem83  39082  fourierdlem84  39083  fourierdlem88  39087  fourierdlem92  39091  fourierdlem93  39092  fourierdlem97  39096  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  sqwvfoura  39121  elaa2lem  39126  etransclem1  39128  etransclem8  39135  etransclem20  39147  etransclem33  39160  etransclem35  39162  etransclem39  39166  rrxtopnfi  39182  ioorrnopnxrlem  39202  sge0tsms  39273  sge0snmpt  39276  sge0fsummpt  39283  sge0pr  39287  sge0lessmpt  39292  sge0iunmptlemfi  39306  sge0iunmptlemre  39308  sge0iunmpt  39311  sge0rpcpnf  39314  sge0isum  39320  nnfoctbdjlem  39348  psmeasure  39364  voliunsge0lem  39365  meaiuninclem  39373  meaiininclem  39376  omeiunltfirp  39409  carageniuncllem2  39412  caratheodorylem1  39416  caratheodorylem2  39417  isomenndlem  39420  hoicvr  39438  hoicvrrex  39446  ovnsupge0  39447  ovnlecvr  39448  ovnf  39453  ovn0lem  39455  ovnsubaddlem1  39460  ovnsubadd  39462  hsphoif  39466  sge0hsphoire  39479  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1lelem3  39483  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem5  39489  ovnhoilem1  39491  ovnhoilem2  39492  ovnlecvr2  39500  ovncvr2  39501  hoidifhspf  39508  hspmbllem2  39517  opnvonmbllem2  39523  ovnsubadd2lem  39535  ovolval4lem1  39539  ovolval4lem2  39540  ovolval5lem2  39543  ovnovollem1  39546  ovnovollem2  39547  iccvonmbllem  39569  vonioolem1  39571  vonioolem2  39572  vonicclem1  39574  vonicclem2  39575  smfid  39639  smfmbfcex  39646  smflim  39663  nsssmfmbflem  39664  smfmullem4  39679  fmtnodvds  39994  pfxf  40252  vtxdgf  40686  crctcsh1wlkn0  41024  1wlkiswwlks2lem5  41070  1wlkpwwlkf1ouspgr  41076  wlknwwlksnfun  41085  wlkwwlkfun  41092  wwlksnextfun  41104  clwlkclwwlklem2a  41207  clwwlksf  41222  clwlksfclwwlk  41269  frgrncvvdeqlem5  41473  av-numclwlk1lem2f  41522  av-numclwlk2lem2f  41533  c0mgm  41699  c0mhm  41700  c0snmgmhm  41704  funcringcsetcALTV2lem3  41830  funcringcsetclem3ALTV  41853  gsumlsscl  41958  ply1mulgsum  41972  lincfsuppcl  41996  linccl  41997  lincvalsc0  42004  lcoc0  42005  linc0scn0  42006  linc1  42008  lincsum  42012  lincscm  42013  lincscmcl  42015  lcoss  42019  lincext1  42037  el0ldep  42049  lincresunit1  42060  lincresunit3  42064  lmod1zr  42076  fdivmptf  42133  refdivmptf  42134  aacllem  42356  amgmwlem  42357  amgmlemALT  42358