Theorem fex 5945

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

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1756   _Vcvv 2967   Fn wfn 5408   -->wf 5409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pr 4526

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421

This theorem is referenced by:  f1oexrnex  6522  frnsuppeq  6697  suppsnop  6699  f1domg  7321  fdmfisuppfi  7621  frnfsuppbi  7640  fsuppco2  7644  fsuppcor  7645  mapfienlem2  7647  ordtypelem10  7733  oiexg  7741  cnfcom3clem  7930  cnfcom3clemOLD  7938  infxpenc2lem2  8178  infxpenc2lem2OLD  8182  fin23lem32  8505  isf32lem10  8523  hashf1rn  12115  hashf1lem1  12200  fz1isolem  12206  climsup  13139  fsum  13189  supcvg  13310  vdwmc  14031  vdwpc  14033  ramval  14061  imasval  14441  imasle  14453  pwsco1mhm  15489  isghm  15738  elsymgbas  15878  gsumval3a  16370  gsumval3lem1  16374  gsumval3lem2  16375  gsumzres  16379  gsumzf1o  16382  gsumzaddlem  16399  gsumzadd  16400  gsumzmhm  16420  gsumzoppg  16430  gsumpt  16443  gsum2dlem2  16450  dmdprd  16468  prdslmodd  17027  gsumply1subr  17663  dsmmsubg  18143  dsmmlss  18144  islindf2  18218  f1lindf  18226  islindf4  18242  prdstps  19177  qtopval2  19244  tsmsres  19693  climcncf  20451  itg2gt0  21213  ulmval  21820  pserulm  21862  jensen  22357  iseupa  23537  isgrpoi  23636  isgrp2d  23673  isgrpda  23735  elghomlem2  23800  isrngod  23817  vcoprne  23908  isvc  23910  isnv  23941  cnnvg  24019  cnnvs  24022  cnnvnm  24023  cncph  24170  ajval  24213  hvmulex  24364  hhph  24531  hlimi  24541  chlimi  24588  hhssva  24611  hhsssm  24612  hhssnm  24613  hhshsslem1  24619  elunop  25227  adjeq  25290  leoprf2  25482  fpwrelmapffslem  25983  lmdvg  26335  esumpfinvallem  26475  ofcfval4  26499  omsfval  26661  eulerpartgbij  26707  eulerpartlemmf  26710  sseqval  26723  subfacp1lem5  27024  sinccvglem  27268  fprod  27405  elno  27738  mbfresfi  28391  filnetlem4  28555  iscringd  28752  climexp  29731  climinf  29732  stirlinglem8  29829  usgra2pth  30254  bj-finsumval0  32426  islaut  33567  ispautN  33583  istendo  34244