Theorem fex 6966

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 6487	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnex 6957	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V)
3	1, 2	sylan 583	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  Vcvv 3441   Fn wfn 6319  ⟶wf 6320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332

This theorem is referenced by:  fexd  6967  f1oexrnex  7614  frnsuppeq  7825  suppsnop  7827  f1domg  8512  fdmfisuppfi  8826  frnfsuppbi  8846  fsuppco2  8850  fsuppcor  8851  mapfienlem2  8853  ordtypelem10  8975  oiexg  8983  cnfcom3clem  9152  infxpenc2lem2  9431  fin23lem32  9755  isf32lem10  9773  focdmex  13707  hasheqf1oi  13708  hashf1rn  13709  hasheqf1od  13710  hashimarn  13797  hashf1lem1  13809  fz1isolem  13815  iswrd  13859  climsup  15018  fsum  15069  supcvg  15203  fprod  15287  vdwmc  16304  vdwpc  16306  ramval  16334  imasval  16776  imasle  16788  pwsco1mhm  17988  isghm  18350  elsymgbas  18494  gsumval3a  19016  gsumval3lem1  19018  gsumval3lem2  19019  gsumzres  19022  gsumzf1o  19025  gsumzaddlem  19034  gsumzadd  19035  gsumzmhm  19050  gsumzoppg  19057  gsumpt  19075  gsum2dlem2  19084  dmdprd  19113  prdslmodd  19734  cnfldfun  20103  cnfldfunALT  20104  dsmmsubg  20432  dsmmlss  20433  islindf2  20503  f1lindf  20511  islindf4  20527  gsumply1subr  20863  prdstps  22234  qtopval2  22301  tsmsres  22749  tngngp3  23262  climcncf  23505  ulmval  24975  pserulm  25017  jensen  25574  isismt  26328  isgrpoi  28281  isvcOLD  28362  isnv  28395  cnnvg  28461  cnnvs  28463  cnnvnm  28464  cncph  28602  ajval  28644  hvmulex  28794  hhph  28961  hlimi  28971  chlimi  29017  hhssva  29040  hhsssm  29041  hhssnm  29042  hhshsslem1  29050  elunop  29655  adjeq  29718  leoprf2  29910  fpwrelmapffslem  30494  pwrssmgc  30706  lmdvg  31306  esumpfinvallem  31443  ofcfval4  31474  omsfval  31662  omsf  31664  omssubadd  31668  carsgval  31671  eulerpartgbij  31740  eulerpartlemmf  31743  sseqval  31756  subfacp1lem5  32544  sinccvglem  33028  elno  33266  filnetlem4  33842  bj-finsumval0  34700  poimirlem24  35081  mbfresfi  35103  elghomlem2OLD  35324  isrngod  35336  isgrpda  35393  iscringd  35436  islaut  37379  ispautN  37395  istendo  38056  binomcxplemnotnn0  41060  fidmfisupp  41828  climexp  42247  climinf  42248  limsupre  42283  stirlinglem8  42723  fourierdlem70  42818  fourierdlem71  42819  fourierdlem80  42828  sge0val  43005  sge0f1o  43021  ismea  43090  meadjiunlem  43104  isomennd  43170  isassintop  44470  fdivmpt  44954  elbigolo1  44971