Theorem fex 6992

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2113  Vcvv 3497   Fn wfn 6353  ⟶wf 6354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pr 5333

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-reu 3148  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366

This theorem is referenced by:  f1oexrnex  7635  frnsuppeq  7845  suppsnop  7847  f1domg  8532  fdmfisuppfi  8845  frnfsuppbi  8865  fsuppco2  8869  fsuppcor  8870  mapfienlem2  8872  ordtypelem10  8994  oiexg  9002  cnfcom3clem  9171  infxpenc2lem2  9449  fin23lem32  9769  isf32lem10  9787  focdmex  13714  hasheqf1oi  13715  hashf1rn  13716  hasheqf1od  13717  hashimarn  13804  hashf1lem1  13816  fz1isolem  13822  iswrd  13866  climsup  15029  fsum  15080  supcvg  15214  fprod  15298  vdwmc  16317  vdwpc  16319  ramval  16347  imasval  16787  imasle  16799  pwsco1mhm  17999  isghm  18361  elsymgbas  18505  gsumval3a  19026  gsumval3lem1  19028  gsumval3lem2  19029  gsumzres  19032  gsumzf1o  19035  gsumzaddlem  19044  gsumzadd  19045  gsumzmhm  19060  gsumzoppg  19067  gsumpt  19085  gsum2dlem2  19094  dmdprd  19123  prdslmodd  19744  gsumply1subr  20405  cnfldfun  20560  cnfldfunALT  20561  dsmmsubg  20890  dsmmlss  20891  islindf2  20961  f1lindf  20969  islindf4  20985  prdstps  22240  qtopval2  22307  tsmsres  22755  tngngp3  23268  climcncf  23511  ulmval  24971  pserulm  25013  jensen  25569  isismt  26323  isgrpoi  28278  isvcOLD  28359  isnv  28392  cnnvg  28458  cnnvs  28460  cnnvnm  28461  cncph  28599  ajval  28641  hvmulex  28791  hhph  28958  hlimi  28968  chlimi  29014  hhssva  29037  hhsssm  29038  hhssnm  29039  hhshsslem1  29047  elunop  29652  adjeq  29715  leoprf2  29907  fpwrelmapffslem  30471  lmdvg  31200  esumpfinvallem  31337  ofcfval4  31368  omsfval  31556  omsf  31558  omssubadd  31562  carsgval  31565  eulerpartgbij  31634  eulerpartlemmf  31637  sseqval  31650  subfacp1lem5  32435  sinccvglem  32919  elno  33157  filnetlem4  33733  bj-finsumval0  34571  poimirlem24  34920  mbfresfi  34942  elghomlem2OLD  35168  isrngod  35180  isgrpda  35237  iscringd  35280  islaut  37223  ispautN  37239  istendo  37900  binomcxplemnotnn0  40694  fexd  41385  fidmfisupp  41468  climexp  41892  climinf  41893  limsupre  41928  stirlinglem8  42373  fourierdlem70  42468  fourierdlem71  42469  fourierdlem80  42478  sge0val  42655  sge0f1o  42671  ismea  42740  meadjiunlem  42754  isomennd  42820  isassintop  44124  fdivmpt  44607  elbigolo1  44624