Theorem fex 7200

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3447   Fn wfn 6506  ⟶wf 6507

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 5234  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519

This theorem is referenced by:  fexd  7201  f1oexrnex  7903  fsuppeq  8154  suppsnop  8157  f1domg  8943  ffsuppbi  9349  mapfienlem2  9357  oiexg  9488  infxpenc2lem2  9973  isf32lem10  10315  hasheqf1oi  14316  hashf1rn  14317  hashimarn  14405  iswrd  14480  climsup  15636  fsum  15686  supcvg  15822  fprod  15907  vdwmc  16949  vdwpc  16951  isghmOLD  19148  elsymgbas  19304  gsumval3a  19833  gsumval3lem1  19835  gsumval3lem2  19836  dmdprd  19930  cnfldfun  21278  cnfldfunALT  21279  cnfldfunOLD  21291  cnfldfunALTOLD  21292  tngngp3  24544  climcncf  24793  ulmval  26289  pserulm  26331  elnoOLD  27558  isismt  28461  isgrpoi  30427  isvcOLD  30508  isnv  30541  cnnvg  30607  cnnvs  30609  cnnvnm  30610  cncph  30748  ajval  30790  hvmulex  30940  hhph  31107  hlimi  31117  chlimi  31163  hhssva  31186  hhsssm  31187  hhssnm  31188  hhshsslem1  31196  elunop  31801  adjeq  31864  leoprf2  32056  fpwrelmapffslem  32655  ccatws1f1o  32873  lmdvg  33943  esumpfinvallem  34064  omsf  34287  eulerpartgbij  34363  eulerpartlemmf  34366  subfacp1lem5  35171  sinccvglem  35659  poimirlem24  37638  mbfresfi  37660  elghomlem2OLD  37880  islaut  40077  ispautN  40093  istendo  40754  binomcxplemnotnn0  44345  climexp  45603  climinf  45604  stirlinglem8  46079  fourierdlem70  46174  ismea  46449  meadjiunlem  46463  grtriclwlk3  47944  isassintop  48198  fdivmpt  48529  elbigolo1  48546  fucofvalne  49314