Theorem fex 7230

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  Vcvv 3451   Fn wfn 6532  ⟶wf 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545

This theorem is used by:  fexd  7231  f1oexrnex  7937  fsuppeq  8185  suppsnop  8188  f1domg  8991  ffsuppbi  9383  mapfienlem2  9391  oiexg  9522  infxpenc2lem2  10092  isf32lem10  10433  hasheqf1oi  14488  hashf1rn  14489  hashimarn  14578  iswrd  14653  climsup  15830  fsum  15879  supcvg  16018  fprod  16101  vdwmc  17149  vdwpc  17151  elsymgbas  19581  gsumval3a  20110  gsumval3lem1  20112  gsumval3lem2  20113  dmdprd  20207  cnfldfun  21685  cnfldfunALT  21686  tngngp3  24968  climcncf  25214  ulmval  26700  pserulm  26742  isismt  28990  isgrpoi  31093  isvcOLD  31174  isnv  31207  cnnvg  31273  cnnvs  31275  cnnvnm  31276  cncph  31414  ajval  31456  hvmulex  31606  hhph  31773  hlimi  31783  chlimi  31829  hhssva  31852  hhsssm  31853  hhssnm  31854  hhshsslem1  31862  elunop  32467  adjeq  32530  leoprf2  32722  fpwrelmapffslem  33317  ccatws1f1o  33507  lmdvg  34578  esumpfinvallem  34699  omsf  34921  eulerpartgbij  34997  eulerpartlemmf  35000  subfacp1lem5  35928  sinccvglem  36416  poimirlem24  38542  mbfresfi  38564  elghomlem2OLD  38800  islaut  41120  ispautN  41136  istendo  41797  binomcxplemnotnn0  45325  climexp  46586  climinf  46587  stirlinglem8  47060  fourierdlem70  47155  ismea  47430  meadjiunlem  47444  grtriclwlk3  49012  isassintop  49276  fdivmpt  49621  elbigolo1  49638  fucofvalne  50402