Theorem fex 7245

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  Vcvv 3477   Fn wfn 6557  ⟶wf 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570

This theorem is referenced by:  fexd  7246  f1oexrnex  7949  fsuppeq  8198  suppsnop  8201  f1domg  9010  ffsuppbi  9435  mapfienlem2  9443  oiexg  9572  infxpenc2lem2  10057  isf32lem10  10399  hasheqf1oi  14386  hashf1rn  14387  hashimarn  14475  iswrd  14550  climsup  15702  fsum  15752  supcvg  15888  fprod  15973  vdwmc  17011  vdwpc  17013  isghmOLD  19246  elsymgbas  19405  gsumval3a  19935  gsumval3lem1  19937  gsumval3lem2  19938  dmdprd  20032  cnfldfun  21395  cnfldfunALT  21396  cnfldfunOLD  21408  cnfldfunALTOLD  21409  cnfldfunALTOLDOLD  21410  tngngp3  24692  climcncf  24939  ulmval  26437  pserulm  26479  elnoOLD  27705  isismt  28556  isgrpoi  30526  isvcOLD  30607  isnv  30640  cnnvg  30706  cnnvs  30708  cnnvnm  30709  cncph  30847  ajval  30889  hvmulex  31039  hhph  31206  hlimi  31216  chlimi  31262  hhssva  31285  hhsssm  31286  hhssnm  31287  hhshsslem1  31295  elunop  31900  adjeq  31963  leoprf2  32155  fpwrelmapffslem  32749  ccatws1f1o  32920  lmdvg  33913  esumpfinvallem  34054  omsf  34277  eulerpartgbij  34353  eulerpartlemmf  34356  subfacp1lem5  35168  sinccvglem  35656  poimirlem24  37630  mbfresfi  37652  elghomlem2OLD  37872  islaut  40065  ispautN  40081  istendo  40742  binomcxplemnotnn0  44351  climexp  45560  climinf  45561  stirlinglem8  46036  fourierdlem70  46131  ismea  46406  meadjiunlem  46420  grtriclwlk3  47849  isassintop  48053  fdivmpt  48389  elbigolo1  48406