Theorem fex 7182

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3444   Fn wfn 6494  ⟶wf 6495

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507

This theorem is referenced by:  fexd  7183  f1oexrnex  7883  fsuppeq  8131  suppsnop  8134  f1domg  8920  ffsuppbi  9325  mapfienlem2  9333  oiexg  9464  infxpenc2lem2  9949  isf32lem10  10291  hasheqf1oi  14292  hashf1rn  14293  hashimarn  14381  iswrd  14456  climsup  15612  fsum  15662  supcvg  15798  fprod  15883  vdwmc  16925  vdwpc  16927  isghmOLD  19124  elsymgbas  19280  gsumval3a  19809  gsumval3lem1  19811  gsumval3lem2  19812  dmdprd  19906  cnfldfun  21254  cnfldfunALT  21255  cnfldfunOLD  21267  cnfldfunALTOLD  21268  tngngp3  24520  climcncf  24769  ulmval  26265  pserulm  26307  elnoOLD  27534  isismt  28437  isgrpoi  30400  isvcOLD  30481  isnv  30514  cnnvg  30580  cnnvs  30582  cnnvnm  30583  cncph  30721  ajval  30763  hvmulex  30913  hhph  31080  hlimi  31090  chlimi  31136  hhssva  31159  hhsssm  31160  hhssnm  31161  hhshsslem1  31169  elunop  31774  adjeq  31837  leoprf2  32029  fpwrelmapffslem  32628  ccatws1f1o  32846  lmdvg  33916  esumpfinvallem  34037  omsf  34260  eulerpartgbij  34336  eulerpartlemmf  34339  subfacp1lem5  35144  sinccvglem  35632  poimirlem24  37611  mbfresfi  37633  elghomlem2OLD  37853  islaut  40050  ispautN  40066  istendo  40727  binomcxplemnotnn0  44318  climexp  45576  climinf  45577  stirlinglem8  46052  fourierdlem70  46147  ismea  46422  meadjiunlem  46436  grtriclwlk3  47917  isassintop  48171  fdivmpt  48502  elbigolo1  48519  fucofvalne  49287