Theorem fex 6052

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 5660	. 2 |- ( F : A --> B -> F Fn A )
2		fnex 6046	. 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 1758   _Vcvv 3071   Fn wfn 5514   -->wf 5515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4504  ax-sep 4514  ax-nul 4522  ax-pr 4632

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-reu 2802  df-rab 2804  df-v 3073  df-sbc 3288  df-csb 3390  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-iun 4274  df-br 4394  df-opab 4452  df-mpt 4453  df-id 4737  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-rn 4952  df-res 4953  df-ima 4954  df-iota 5482  df-fun 5521  df-fn 5522  df-f 5523  df-f1 5524  df-fo 5525  df-f1o 5526  df-fv 5527

This theorem is referenced by:  f1oexrnex  6630  frnsuppeq  6805  suppsnop  6807  f1domg  7432  fdmfisuppfi  7733  frnfsuppbi  7752  fsuppco2  7756  fsuppcor  7757  mapfienlem2  7759  ordtypelem10  7845  oiexg  7853  cnfcom3clem  8042  cnfcom3clemOLD  8050  infxpenc2lem2  8290  infxpenc2lem2OLD  8294  fin23lem32  8617  isf32lem10  8635  hashf1rn  12233  hashf1lem1  12319  fz1isolem  12325  climsup  13258  fsum  13308  supcvg  13429  vdwmc  14150  vdwpc  14152  ramval  14180  imasval  14560  imasle  14572  pwsco1mhm  15609  isghm  15858  elsymgbas  15998  gsumval3a  16492  gsumval3lem1  16496  gsumval3lem2  16497  gsumzres  16501  gsumzf1o  16504  gsumzaddlem  16521  gsumzadd  16522  gsumzmhm  16544  gsumzoppg  16554  gsumpt  16568  gsum2dlem2  16576  dmdprd  16594  prdslmodd  17165  gsumply1subr  17804  dsmmsubg  18286  dsmmlss  18287  islindf2  18361  f1lindf  18369  islindf4  18385  prdstps  19327  qtopval2  19394  tsmsres  19843  climcncf  20601  itg2gt0  21364  ulmval  21971  pserulm  22013  jensen  22508  iseupa  23731  isgrpoi  23830  isgrp2d  23867  isgrpda  23929  elghomlem2  23994  isrngod  24011  vcoprne  24102  isvc  24104  isnv  24135  cnnvg  24213  cnnvs  24216  cnnvnm  24217  cncph  24364  ajval  24407  hvmulex  24558  hhph  24725  hlimi  24735  chlimi  24782  hhssva  24805  hhsssm  24806  hhssnm  24807  hhshsslem1  24813  elunop  25421  adjeq  25484  leoprf2  25676  fpwrelmapffslem  26176  lmdvg  26521  esumpfinvallem  26661  ofcfval4  26685  omsfval  26846  eulerpartgbij  26892  eulerpartlemmf  26895  sseqval  26908  subfacp1lem5  27209  sinccvglem  27454  fprod  27591  elno  27924  mbfresfi  28579  filnetlem4  28743  iscringd  28940  climexp  29919  climinf  29920  stirlinglem8  30017  usgra2pth  30442  bj-finsumval0  32892  islaut  34036  ispautN  34052  istendo  34713