MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fex Unicode version

Theorem fex 5790
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  |-  ( ( F : A --> B  /\  A  e.  C )  ->  F  e.  _V )

Proof of Theorem fex
StepHypRef Expression
1 ffn 5427 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnex 5782 . 2  |-  ( ( F  Fn  A  /\  A  e.  C )  ->  F  e.  _V )
31, 2sylan 457 1  |-  ( ( F : A --> B  /\  A  e.  C )  ->  F  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1701   _Vcvv 2822    Fn wfn 5287   -->wf 5288
This theorem is referenced by:  f1domg  6924  ordtypelem10  7287  oiexg  7295  cnfcom3clem  7453  infxpenc2lem2  7692  fin23lem32  8015  isf32lem10  8033  hashf1lem1  11440  fz1isolem  11446  climsup  12190  fsum  12240  supcvg  12361  vdwmc  13072  vdwpc  13074  ramval  13102  imasval  13463  imasle  13474  pwsco1mhm  14495  isghm  14732  elsymgbas  14823  dmdprd  15285  prdslmodd  15775  prdstps  17379  qtopval2  17443  climcncf  18456  itg2gt0  19168  ulmval  19812  pserulm  19851  jensen  20336  isgrpoi  20918  isgrp2d  20955  isgrpda  21017  elghomlem2  21082  isrngod  21099  vcoprne  21190  isvc  21192  isnv  21223  cnnvg  21301  cnnvs  21304  cnnvnm  21305  cncph  21452  ajval  21495  hvmulex  21646  hhph  21812  hlimi  21822  chlimi  21869  hhssva  21891  hhsssm  21892  hhssnm  21893  hhshsslem1  21899  elunop  22507  adjeq  22570  leoprf2  22762  lmdvg  23407  esumpfinvallem  23640  ofcfval4  23664  subfacp1lem5  23999  iseupa  24165  sinccvglem  24289  fprod  24444  elno  24685  filnetlem4  25479  iscringd  25772  dsmmsubg  26357  dsmmlss  26358  islindf2  26432  f1lindf  26440  islindf4  26456  climexp  26879  climinf  26880  stirlinglem8  26978  islaut  30090  ispautN  30106  istendo  30767
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-rep 4168  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-reu 2584  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-iun 3944  df-br 4061  df-opab 4115  df-mpt 4116  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300
  Copyright terms: Public domain W3C validator