Theorem fex 7246

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3480   Fn wfn 6556  ⟶wf 6557

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 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569

This theorem is referenced by:  fexd  7247  f1oexrnex  7949  fsuppeq  8200  suppsnop  8203  f1domg  9012  ffsuppbi  9438  mapfienlem2  9446  oiexg  9575  infxpenc2lem2  10060  isf32lem10  10402  hasheqf1oi  14390  hashf1rn  14391  hashimarn  14479  iswrd  14554  climsup  15706  fsum  15756  supcvg  15892  fprod  15977  vdwmc  17016  vdwpc  17018  isghmOLD  19234  elsymgbas  19391  gsumval3a  19921  gsumval3lem1  19923  gsumval3lem2  19924  dmdprd  20018  cnfldfun  21378  cnfldfunALT  21379  cnfldfunOLD  21391  cnfldfunALTOLD  21392  cnfldfunALTOLDOLD  21393  tngngp3  24677  climcncf  24926  ulmval  26423  pserulm  26465  elnoOLD  27691  isismt  28542  isgrpoi  30517  isvcOLD  30598  isnv  30631  cnnvg  30697  cnnvs  30699  cnnvnm  30700  cncph  30838  ajval  30880  hvmulex  31030  hhph  31197  hlimi  31207  chlimi  31253  hhssva  31276  hhsssm  31277  hhssnm  31278  hhshsslem1  31286  elunop  31891  adjeq  31954  leoprf2  32146  fpwrelmapffslem  32743  ccatws1f1o  32936  lmdvg  33952  esumpfinvallem  34075  omsf  34298  eulerpartgbij  34374  eulerpartlemmf  34377  subfacp1lem5  35189  sinccvglem  35677  poimirlem24  37651  mbfresfi  37673  elghomlem2OLD  37893  islaut  40085  ispautN  40101  istendo  40762  binomcxplemnotnn0  44375  climexp  45620  climinf  45621  stirlinglem8  46096  fourierdlem70  46191  ismea  46466  meadjiunlem  46480  grtriclwlk3  47912  isassintop  48126  fdivmpt  48461  elbigolo1  48478  fucofvalne  49020