Theorem fex 6750

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	⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V)

Proof of Theorem fex

Step	Hyp	Ref	Expression
1		ffn 6282	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnex 6742	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V)
3	1, 2	sylan 575	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V)

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2164  Vcvv 3414   Fn wfn 6122  ⟶wf 6123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4996  ax-sep 5007  ax-nul 5015  ax-pr 5129

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-sn 4400  df-pr 4402  df-op 4406  df-uni 4661  df-iun 4744  df-br 4876  df-opab 4938  df-mpt 4955  df-id 5252  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135

This theorem is referenced by:  f1oexrnex  7382  frnsuppeq  7576  suppsnop  7578  f1domg  8248  fdmfisuppfi  8559  frnfsuppbi  8579  fsuppco2  8583  fsuppcor  8584  mapfienlem2  8586  ordtypelem10  8708  oiexg  8716  cnfcom3clem  8886  infxpenc2lem2  9163  fin23lem32  9488  isf32lem10  9506  focdmex  13438  hasheqf1oi  13439  hashf1rn  13440  hasheqf1od  13441  hashimarn  13523  hashf1lem1  13535  fz1isolem  13541  iswrd  13583  climsup  14784  fsum  14835  supcvg  14969  fprod  15051  vdwmc  16060  vdwpc  16062  ramval  16090  imasval  16531  imasle  16543  pwsco1mhm  17730  isghm  18018  elsymgbas  18159  gsumval3a  18664  gsumval3lem1  18666  gsumval3lem2  18667  gsumzres  18670  gsumzf1o  18673  gsumzaddlem  18681  gsumzadd  18682  gsumzmhm  18697  gsumzoppg  18704  gsumpt  18721  gsum2dlem2  18730  dmdprd  18758  prdslmodd  19335  gsumply1subr  19971  cnfldfun  20125  cnfldfunALT  20126  dsmmsubg  20457  dsmmlss  20458  islindf2  20527  f1lindf  20535  islindf4  20551  prdstps  21810  qtopval2  21877  tsmsres  22324  tngngp3  22837  climcncf  23080  itg2gt0  23933  ulmval  24540  pserulm  24582  jensen  25135  isismt  25853  isgrpoi  27904  isvcOLD  27985  isnv  28018  cnnvg  28084  cnnvs  28086  cnnvnm  28087  cncph  28225  ajval  28268  hvmulex  28419  hhph  28586  hlimi  28596  chlimi  28642  hhssva  28665  hhsssm  28666  hhssnm  28667  hhshsslem1  28675  elunop  29282  adjeq  29345  leoprf2  29537  fpwrelmapffslem  30051  lmdvg  30540  esumpfinvallem  30677  ofcfval4  30708  omsfval  30897  omsf  30899  omssubadd  30903  carsgval  30906  eulerpartgbij  30975  eulerpartlemmf  30978  sseqval  30992  subfacp1lem5  31708  sinccvglem  32106  elno  32333  filnetlem4  32909  bj-finsumval0  33694  poimirlem24  33972  mbfresfi  33994  elghomlem2OLD  34222  isrngod  34234  isgrpda  34291  iscringd  34334  islaut  36153  ispautN  36169  istendo  36830  binomcxplemnotnn0  39390  fexd  40106  fidmfisupp  40192  climexp  40626  climinf  40627  limsupre  40662  stirlinglem8  41086  fourierdlem70  41181  fourierdlem71  41182  fourierdlem80  41191  sge0val  41368  sge0f1o  41384  ismea  41453  meadjiunlem  41467  isomennd  41533  isassintop  42707  fdivmpt  43195  elbigolo1  43212