Theorem fex 7205

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  Vcvv 3453   Fn wfn 6511  ⟶wf 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5224  ax-sep 5243  ax-nul 5253  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524

This theorem is referenced by:  fexd  7206  f1oexrnex  7903  fsuppeq  8149  suppsnop  8152  f1domg  8946  ffsuppbi  9338  mapfienlem2  9346  oiexg  9477  infxpenc2lem2  9970  isf32lem10  10313  hasheqf1oi  14358  hashf1rn  14359  hashimarn  14447  iswrd  14522  climsup  15688  fsum  15738  supcvg  15877  fprod  15962  vdwmc  17005  vdwpc  17007  elsymgbas  19405  gsumval3a  19934  gsumval3lem1  19936  gsumval3lem2  19937  dmdprd  20031  cnfldfun  21426  cnfldfunALT  21427  tngngp3  24704  climcncf  24950  ulmval  26431  pserulm  26473  isismt  28691  isgrpoi  30658  isvcOLD  30739  isnv  30772  cnnvg  30838  cnnvs  30840  cnnvnm  30841  cncph  30979  ajval  31021  hvmulex  31171  hhph  31338  hlimi  31348  chlimi  31394  hhssva  31417  hhsssm  31418  hhssnm  31419  hhshsslem1  31427  elunop  32032  adjeq  32095  leoprf2  32287  fpwrelmapffslem  32895  ccatws1f1o  33090  lmdvg  34211  esumpfinvallem  34332  omsf  34554  eulerpartgbij  34630  eulerpartlemmf  34633  subfacp1lem5  35495  sinccvglem  35983  poimirlem24  38104  mbfresfi  38126  elghomlem2OLD  38346  islaut  40668  ispautN  40684  istendo  41345  binomcxplemnotnn0  44893  climexp  46142  climinf  46143  stirlinglem8  46616  fourierdlem70  46711  ismea  46986  meadjiunlem  47000  grtriclwlk3  48528  isassintop  48793  fdivmpt  49123  elbigolo1  49140  fucofvalne  49907