Theorem fex 7203

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3450   Fn wfn 6509  ⟶wf 6510

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 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522

This theorem is referenced by:  fexd  7204  f1oexrnex  7906  fsuppeq  8157  suppsnop  8160  f1domg  8946  ffsuppbi  9356  mapfienlem2  9364  oiexg  9495  infxpenc2lem2  9980  isf32lem10  10322  hasheqf1oi  14323  hashf1rn  14324  hashimarn  14412  iswrd  14487  climsup  15643  fsum  15693  supcvg  15829  fprod  15914  vdwmc  16956  vdwpc  16958  isghmOLD  19155  elsymgbas  19311  gsumval3a  19840  gsumval3lem1  19842  gsumval3lem2  19843  dmdprd  19937  cnfldfun  21285  cnfldfunALT  21286  cnfldfunOLD  21298  cnfldfunALTOLD  21299  tngngp3  24551  climcncf  24800  ulmval  26296  pserulm  26338  elnoOLD  27565  isismt  28468  isgrpoi  30434  isvcOLD  30515  isnv  30548  cnnvg  30614  cnnvs  30616  cnnvnm  30617  cncph  30755  ajval  30797  hvmulex  30947  hhph  31114  hlimi  31124  chlimi  31170  hhssva  31193  hhsssm  31194  hhssnm  31195  hhshsslem1  31203  elunop  31808  adjeq  31871  leoprf2  32063  fpwrelmapffslem  32662  ccatws1f1o  32880  lmdvg  33950  esumpfinvallem  34071  omsf  34294  eulerpartgbij  34370  eulerpartlemmf  34373  subfacp1lem5  35178  sinccvglem  35666  poimirlem24  37645  mbfresfi  37667  elghomlem2OLD  37887  islaut  40084  ispautN  40100  istendo  40761  binomcxplemnotnn0  44352  climexp  45610  climinf  45611  stirlinglem8  46086  fourierdlem70  46181  ismea  46456  meadjiunlem  46470  grtriclwlk3  47948  isassintop  48202  fdivmpt  48533  elbigolo1  48550  fucofvalne  49318