Theorem fex 7169

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Vcvv 3437   Fn wfn 6484  ⟶wf 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497

This theorem is referenced by:  fexd  7170  f1oexrnex  7866  fsuppeq  8114  suppsnop  8117  f1domg  8904  ffsuppbi  9293  mapfienlem2  9301  oiexg  9432  infxpenc2lem2  9922  isf32lem10  10264  hasheqf1oi  14265  hashf1rn  14266  hashimarn  14354  iswrd  14429  climsup  15584  fsum  15634  supcvg  15770  fprod  15855  vdwmc  16897  vdwpc  16899  isghmOLD  19136  elsymgbas  19294  gsumval3a  19823  gsumval3lem1  19825  gsumval3lem2  19826  dmdprd  19920  cnfldfun  21314  cnfldfunALT  21315  cnfldfunOLD  21327  cnfldfunALTOLD  21328  tngngp3  24591  climcncf  24840  ulmval  26336  pserulm  26378  elnoOLD  27605  isismt  28532  isgrpoi  30499  isvcOLD  30580  isnv  30613  cnnvg  30679  cnnvs  30681  cnnvnm  30682  cncph  30820  ajval  30862  hvmulex  31012  hhph  31179  hlimi  31189  chlimi  31235  hhssva  31258  hhsssm  31259  hhssnm  31260  hhshsslem1  31268  elunop  31873  adjeq  31936  leoprf2  32128  fpwrelmapffslem  32739  ccatws1f1o  32961  lmdvg  34038  esumpfinvallem  34159  omsf  34381  eulerpartgbij  34457  eulerpartlemmf  34460  subfacp1lem5  35300  sinccvglem  35788  poimirlem24  37757  mbfresfi  37779  elghomlem2OLD  37999  islaut  40255  ispautN  40271  istendo  40932  binomcxplemnotnn0  44513  climexp  45767  climinf  45768  stirlinglem8  46241  fourierdlem70  46336  ismea  46611  meadjiunlem  46625  grtriclwlk3  48107  isassintop  48372  fdivmpt  48702  elbigolo1  48719  fucofvalne  49486