Theorem fex 6490

Description: If the domain of a mapping is a set, the function is a set. (Contributed by NM, 3-Oct-1999.)

Assertion

Ref	Expression
fex	|- ( ( F : A --> B /\ A e. C ) -> F e. _V )

Proof of Theorem fex

Step	Hyp	Ref	Expression
1		ffn 6045	. 2 |- ( F : A --> B -> F Fn A )
2		fnex 6481	. 2 |- ( ( F Fn A /\ A e. C ) -> F e. _V )
3	1, 2	sylan 488	1 |- ( ( F : A --> B /\ A e. C ) -> F e. _V )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   _Vcvv 3200   Fn wfn 5883   -->wf 5884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896

This theorem is referenced by:  f1oexrnex  7115  frnsuppeq  7307  suppsnop  7309  f1domg  7975  fdmfisuppfi  8284  frnfsuppbi  8304  fsuppco2  8308  fsuppcor  8309  mapfienlem2  8311  ordtypelem10  8432  oiexg  8440  cnfcom3clem  8602  infxpenc2lem2  8843  fin23lem32  9166  isf32lem10  9184  focdmex  13139  hasheqf1oi  13140  hashf1rn  13142  hashf1rnOLD  13143  hasheqf1od  13144  hashimarn  13227  hashf1lem1  13239  fz1isolem  13245  iswrd  13307  climsup  14400  fsum  14451  supcvg  14588  fprod  14671  vdwmc  15682  vdwpc  15684  ramval  15712  imasval  16171  imasle  16183  pwsco1mhm  17370  isghm  17660  elsymgbas  17802  gsumval3a  18304  gsumval3lem1  18306  gsumval3lem2  18307  gsumzres  18310  gsumzf1o  18313  gsumzaddlem  18321  gsumzadd  18322  gsumzmhm  18337  gsumzoppg  18344  gsumpt  18361  gsum2dlem2  18370  dmdprd  18397  prdslmodd  18969  gsumply1subr  19604  cnfldfun  19758  cnfldfunALT  19759  dsmmsubg  20087  dsmmlss  20088  islindf2  20153  f1lindf  20161  islindf4  20177  prdstps  21432  qtopval2  21499  tsmsres  21947  tngngp3  22460  climcncf  22703  itg2gt0  23527  ulmval  24134  pserulm  24176  jensen  24715  isismt  25429  isgrpoi  27352  isvcOLD  27434  isnv  27467  cnnvg  27533  cnnvs  27535  cnnvnm  27536  cncph  27674  ajval  27717  hvmulex  27868  hhph  28035  hlimi  28045  chlimi  28091  hhssva  28114  hhsssm  28115  hhssnm  28116  hhshsslem1  28124  elunop  28731  adjeq  28794  leoprf2  28986  fpwrelmapffslem  29507  lmdvg  29999  esumpfinvallem  30136  ofcfval4  30167  omsfval  30356  omsf  30358  omssubadd  30362  carsgval  30365  eulerpartgbij  30434  eulerpartlemmf  30437  sseqval  30450  subfacp1lem5  31166  sinccvglem  31566  elno  31799  filnetlem4  32376  bj-finsumval0  33147  poimirlem24  33433  mbfresfi  33456  elghomlem2OLD  33685  isrngod  33697  isgrpda  33754  iscringd  33797  islaut  35369  ispautN  35385  istendo  36048  binomcxplemnotnn0  38555  fexd  39296  fidmfisupp  39390  climexp  39837  climinf  39838  limsupre  39873  stirlinglem8  40298  fourierdlem70  40393  fourierdlem71  40394  fourierdlem80  40403  sge0val  40583  sge0f1o  40599  ismea  40668  meadjiunlem  40682  isomennd  40745  isassintop  41846  fdivmpt  42334  elbigolo1  42351