Theorem fex 6097

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

Syntax hints:   -> wi 4   /\ wa 370   e. wcel 1872   _Vcvv 3022   Fn wfn 5539   -->wf 5540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pr 4603

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-reu 2721  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-id 4711  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552

This theorem is referenced by:  f1oexrnex  6700  frnsuppeq  6881  suppsnop  6883  f1domg  7543  fdmfisuppfi  7845  frnfsuppbi  7865  fsuppco2  7869  fsuppcor  7870  mapfienlem2  7872  ordtypelem10  7995  oiexg  8003  cnfcom3clem  8162  infxpenc2lem2  8402  fin23lem32  8725  isf32lem10  8743  hashf1rn  12485  hashf1lem1  12566  fz1isolem  12572  iswrd  12620  climsup  13676  fsum  13729  supcvg  13857  fprod  13938  vdwmc  14871  vdwpc  14873  ramval  14903  ramvalOLD  14904  imasval  15354  imasvalOLD  15355  imasle  15367  pwsco1mhm  16560  isghm  16826  elsymgbas  16966  gsumval3a  17480  gsumval3lem1  17482  gsumval3lem2  17483  gsumzres  17486  gsumzf1o  17489  gsumzaddlem  17497  gsumzadd  17498  gsumzmhm  17513  gsumzoppg  17520  gsumpt  17537  gsum2dlem2  17546  dmdprd  17573  prdslmodd  18135  gsumply1subr  18770  dsmmsubg  19248  dsmmlss  19249  islindf2  19314  f1lindf  19322  islindf4  19338  prdstps  20586  qtopval2  20653  tsmsres  21100  climcncf  21874  itg2gt0  22660  ulmval  23277  pserulm  23319  jensen  23856  isismt  24521  iseupa  25635  isgrpoi  25868  isgrp2d  25905  isgrpda  25967  elghomlem2OLD  26032  isrngod  26049  vcoprne  26140  isvc  26142  isnv  26173  cnnvg  26251  cnnvs  26254  cnnvnm  26255  cncph  26402  ajval  26445  hvmulex  26606  hhph  26773  hlimi  26783  chlimi  26829  hhssva  26852  hhsssm  26853  hhssnm  26854  hhshsslem1  26860  elunop  27467  adjeq  27530  leoprf2  27722  fpwrelmapffslem  28267  lmdvg  28711  esumpfinvallem  28847  ofcfval4  28878  omsfval  29070  omsf  29072  omsfvalOLD  29074  omsfOLD  29076  omssubadd  29080  omssubaddOLD  29084  carsgval  29087  eulerpartgbij  29157  eulerpartlemmf  29160  sseqval  29173  subfacp1lem5  29859  sinccvglem  30268  elno  30484  filnetlem4  30986  bj-finsumval0  31609  poimirlem24  31871  mbfresfi  31894  iscringd  32139  islaut  33560  ispautN  33576  istendo  34239  binomcxplemnotnn0  36618  climexp  37566  climinf  37567  climinfOLD  37568  limsupre  37604  limsupreOLD  37605  stirlinglem8  37826  fourierdlem70  37923  fourierdlem71  37924  fourierdlem80  37933  sge0val  38059  sge0f1o  38075  ismea  38140  meadjiunlem  38154  isomennd  38203  usgra2pth  39269  isassintop  39447  fdivmpt  39954  elbigolo1  39971