Theorem fex 7263

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3488   Fn wfn 6568  ⟶wf 6569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581

This theorem is referenced by:  fexd  7264  f1oexrnex  7967  fsuppeq  8216  suppsnop  8219  f1domg  9032  ffsuppbi  9467  mapfienlem2  9475  oiexg  9604  infxpenc2lem2  10089  isf32lem10  10431  hasheqf1oi  14400  hashf1rn  14401  hashimarn  14489  iswrd  14564  climsup  15718  fsum  15768  supcvg  15904  fprod  15989  vdwmc  17025  vdwpc  17027  isghmOLD  19256  elsymgbas  19415  gsumval3a  19945  gsumval3lem1  19947  gsumval3lem2  19948  dmdprd  20042  cnfldfun  21401  cnfldfunALT  21402  cnfldfunOLD  21414  cnfldfunALTOLD  21415  cnfldfunALTOLDOLD  21416  tngngp3  24698  climcncf  24945  ulmval  26441  pserulm  26483  elnoOLD  27709  isismt  28560  isgrpoi  30530  isvcOLD  30611  isnv  30644  cnnvg  30710  cnnvs  30712  cnnvnm  30713  cncph  30851  ajval  30893  hvmulex  31043  hhph  31210  hlimi  31220  chlimi  31266  hhssva  31289  hhsssm  31290  hhssnm  31291  hhshsslem1  31299  elunop  31904  adjeq  31967  leoprf2  32159  fpwrelmapffslem  32746  ccatws1f1o  32918  lmdvg  33899  esumpfinvallem  34038  omsf  34261  eulerpartgbij  34337  eulerpartlemmf  34340  subfacp1lem5  35152  sinccvglem  35640  poimirlem24  37604  mbfresfi  37626  elghomlem2OLD  37846  islaut  40040  ispautN  40056  istendo  40717  binomcxplemnotnn0  44325  climexp  45526  climinf  45527  stirlinglem8  46002  fourierdlem70  46097  ismea  46372  meadjiunlem  46386  grtriclwlk3  47796  isassintop  47933  fdivmpt  48274  elbigolo1  48291