Theorem fex 6394

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  Vcvv 3173   Fn wfn 5799  ⟶wf 5800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812

This theorem is referenced by:  f1oexrnex  7008  frnsuppeq  7194  suppsnop  7196  f1domg  7861  fdmfisuppfi  8167  frnfsuppbi  8187  fsuppco2  8191  fsuppcor  8192  mapfienlem2  8194  ordtypelem10  8315  oiexg  8323  cnfcom3clem  8485  infxpenc2lem2  8726  fin23lem32  9049  isf32lem10  9067  focdmex  13001  hasheqf1oi  13002  hashf1rn  13004  hashf1rnOLD  13005  hasheqf1od  13006  hashimarn  13085  hashf1lem1  13096  fz1isolem  13102  iswrd  13162  climsup  14248  fsum  14298  supcvg  14427  fprod  14510  vdwmc  15520  vdwpc  15522  ramval  15550  imasval  15994  imasle  16006  pwsco1mhm  17193  isghm  17483  elsymgbas  17625  gsumval3a  18127  gsumval3lem1  18129  gsumval3lem2  18130  gsumzres  18133  gsumzf1o  18136  gsumzaddlem  18144  gsumzadd  18145  gsumzmhm  18160  gsumzoppg  18167  gsumpt  18184  gsum2dlem2  18193  dmdprd  18220  prdslmodd  18790  gsumply1subr  19425  dsmmsubg  19906  dsmmlss  19907  islindf2  19972  f1lindf  19980  islindf4  19996  prdstps  21242  qtopval2  21309  tsmsres  21757  tngngp3  22270  climcncf  22511  itg2gt0  23333  ulmval  23938  pserulm  23980  jensen  24515  isismt  25229  iseupa  26492  isgrpoi  26736  isvcOLD  26818  isnv  26851  cnnvg  26917  cnnvs  26919  cnnvnm  26920  cncph  27058  ajval  27101  hvmulex  27252  hhph  27419  hlimi  27429  chlimi  27475  hhssva  27498  hhsssm  27499  hhssnm  27500  hhshsslem1  27508  elunop  28115  adjeq  28178  leoprf2  28370  fpwrelmapffslem  28895  lmdvg  29327  esumpfinvallem  29463  ofcfval4  29494  omsfval  29683  omsf  29685  omssubadd  29689  carsgval  29692  eulerpartgbij  29761  eulerpartlemmf  29764  sseqval  29777  subfacp1lem5  30420  sinccvglem  30820  elno  31043  filnetlem4  31546  bj-finsumval0  32324  poimirlem24  32603  mbfresfi  32626  elghomlem2OLD  32855  isrngod  32867  isgrpda  32924  iscringd  32967  islaut  34387  ispautN  34403  istendo  35066  binomcxplemnotnn0  37577  fexd  38327  fidmfisupp  38385  climexp  38672  climinf  38673  limsupre  38708  stirlinglem8  38974  fourierdlem70  39069  fourierdlem71  39070  fourierdlem80  39079  sge0val  39259  sge0f1o  39275  ismea  39344  meadjiunlem  39358  isomennd  39421  usgr2pth  40970  isassintop  41636  fdivmpt  42132  elbigolo1  42149