Theorem fex 6120

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

Syntax hints:   -> wi 4   /\ wa 367   e. wcel 1823   _Vcvv 3106   Fn wfn 5565   -->wf 5566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578

This theorem is referenced by:  f1oexrnex  6722  frnsuppeq  6903  suppsnop  6905  f1domg  7528  fdmfisuppfi  7830  frnfsuppbi  7850  fsuppco2  7854  fsuppcor  7855  mapfienlem2  7857  ordtypelem10  7944  oiexg  7952  cnfcom3clem  8140  cnfcom3clemOLD  8148  infxpenc2lem2  8388  infxpenc2lem2OLD  8392  fin23lem32  8715  isf32lem10  8733  hashf1rn  12410  hashf1lem1  12491  fz1isolem  12497  iswrd  12537  climsup  13577  fsum  13627  supcvg  13752  fprod  13833  vdwmc  14583  vdwpc  14585  ramval  14613  imasval  15003  imasle  15015  pwsco1mhm  16203  isghm  16469  elsymgbas  16609  gsumval3a  17107  gsumval3lem1  17111  gsumval3lem2  17112  gsumzres  17116  gsumzf1o  17119  gsumzaddlem  17136  gsumzadd  17137  gsumzmhm  17158  gsumzoppg  17168  gsumpt  17187  gsum2dlem2  17197  dmdprd  17227  prdslmodd  17813  gsumply1subr  18473  dsmmsubg  18950  dsmmlss  18951  islindf2  19019  f1lindf  19027  islindf4  19043  prdstps  20299  qtopval2  20366  tsmsres  20815  climcncf  21573  itg2gt0  22336  ulmval  22944  pserulm  22986  jensen  23519  isismt  24125  iseupa  25170  isgrpoi  25401  isgrp2d  25438  isgrpda  25500  elghomlem2OLD  25565  isrngod  25582  vcoprne  25673  isvc  25675  isnv  25706  cnnvg  25784  cnnvs  25787  cnnvnm  25788  cncph  25935  ajval  25978  hvmulex  26129  hhph  26296  hlimi  26306  chlimi  26353  hhssva  26376  hhsssm  26377  hhssnm  26378  hhshsslem1  26384  elunop  26992  adjeq  27055  leoprf2  27247  fpwrelmapffslem  27789  lmdvg  28173  esumpfinvallem  28306  ofcfval4  28337  omsfval  28505  omsf  28507  omssubadd  28511  carsgval  28514  eulerpartgbij  28578  eulerpartlemmf  28581  sseqval  28594  subfacp1lem5  28895  sinccvglem  29305  elno  29649  mbfresfi  30304  filnetlem4  30442  iscringd  30639  binomcxplemnotnn0  31505  climexp  31853  climinf  31854  limsupre  31889  stirlinglem8  32105  fourierdlem70  32201  fourierdlem71  32202  fourierdlem80  32211  usgra2pth  32745  isassintop  32925  fdivmpt  33434  elbigolo1  33451  bj-finsumval0  35082  islaut  36223  ispautN  36239  istendo  36902