Theorem fex 6162

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 5750	. 2 |- ( F : A --> B -> F Fn A )
2		fnex 6156	. 2 |- ( ( F Fn A /\ A e. C ) -> F e. _V )
3	1, 2	sylan 478	1 |- ( ( F : A --> B /\ A e. C ) -> F e. _V )

Syntax hints:   -> wi 4   /\ wa 375   e. wcel 1897   _Vcvv 3056   Fn wfn 5595   -->wf 5596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pr 4652

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-reu 2755  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608

This theorem is referenced by:  f1oexrnex  6768  frnsuppeq  6952  suppsnop  6954  f1domg  7614  fdmfisuppfi  7917  frnfsuppbi  7937  fsuppco2  7941  fsuppcor  7942  mapfienlem2  7944  ordtypelem10  8067  oiexg  8075  cnfcom3clem  8235  infxpenc2lem2  8476  fin23lem32  8799  isf32lem10  8817  hashf1rn  12566  hashf1lem1  12650  fz1isolem  12656  iswrd  12704  climsup  13781  fsum  13834  supcvg  13962  fprod  14043  vdwmc  14976  vdwpc  14978  ramval  15008  ramvalOLD  15009  imasval  15459  imasvalOLD  15460  imasle  15472  pwsco1mhm  16665  isghm  16931  elsymgbas  17071  gsumval3a  17585  gsumval3lem1  17587  gsumval3lem2  17588  gsumzres  17591  gsumzf1o  17594  gsumzaddlem  17602  gsumzadd  17603  gsumzmhm  17618  gsumzoppg  17625  gsumpt  17642  gsum2dlem2  17651  dmdprd  17678  prdslmodd  18240  gsumply1subr  18875  dsmmsubg  19354  dsmmlss  19355  islindf2  19420  f1lindf  19428  islindf4  19444  prdstps  20692  qtopval2  20759  tsmsres  21206  climcncf  21980  itg2gt0  22766  ulmval  23383  pserulm  23425  jensen  23962  isismt  24627  iseupa  25741  isgrpoi  25974  isgrp2d  26011  isgrpda  26073  elghomlem2OLD  26138  isrngod  26155  vcoprne  26246  isvc  26248  isnv  26279  cnnvg  26357  cnnvs  26360  cnnvnm  26361  cncph  26508  ajval  26551  hvmulex  26712  hhph  26879  hlimi  26889  chlimi  26935  hhssva  26958  hhsssm  26959  hhssnm  26960  hhshsslem1  26966  elunop  27573  adjeq  27636  leoprf2  27828  fpwrelmapffslem  28365  lmdvg  28807  esumpfinvallem  28943  ofcfval4  28974  omsfval  29166  omsf  29168  omsfvalOLD  29170  omsfOLD  29172  omssubadd  29176  omssubaddOLD  29180  carsgval  29183  eulerpartgbij  29253  eulerpartlemmf  29256  sseqval  29269  subfacp1lem5  29955  sinccvglem  30364  elno  30581  filnetlem4  31085  bj-finsumval0  31746  poimirlem24  32008  mbfresfi  32031  iscringd  32276  islaut  33692  ispautN  33708  istendo  34371  binomcxplemnotnn0  36748  fidmfisupp  37516  climexp  37720  climinf  37721  climinfOLD  37722  limsupre  37758  limsupreOLD  37759  stirlinglem8  37980  fourierdlem70  38077  fourierdlem71  38078  fourierdlem80  38087  sge0val  38245  sge0f1o  38261  ismea  38326  meadjiunlem  38340  isomennd  38389  usgra2pth  39940  isassintop  40118  fdivmpt  40623  elbigolo1  40640