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

Theorem fex 6145
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

Proof of Theorem fex
StepHypRef Expression
1 ffn 5736 . 2
2 fnex 6139 . 2
31, 2sylan 471 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818   cvv 3109  Fnwfn 5588  -->wf 5589
This theorem is referenced by:  f1oexrnex  6749  frnsuppeq  6930  suppsnop  6932  f1domg  7555  fdmfisuppfi  7858  frnfsuppbi  7878  fsuppco2  7882  fsuppcor  7883  mapfienlem2  7885  ordtypelem10  7973  oiexg  7981  cnfcom3clem  8170  cnfcom3clemOLD  8178  infxpenc2lem2  8418  infxpenc2lem2OLD  8422  fin23lem32  8745  isf32lem10  8763  hashf1rn  12425  hashf1lem1  12504  fz1isolem  12510  climsup  13492  fsum  13542  supcvg  13667  fprod  13748  vdwmc  14496  vdwpc  14498  ramval  14526  imasval  14908  imasle  14920  pwsco1mhm  16001  isghm  16267  elsymgbas  16407  gsumval3a  16905  gsumval3lem1  16909  gsumval3lem2  16910  gsumzres  16914  gsumzf1o  16917  gsumzaddlem  16934  gsumzadd  16935  gsumzmhm  16957  gsumzoppg  16967  gsumpt  16988  gsum2dlem2  16998  dmdprd  17029  prdslmodd  17615  gsumply1subr  18275  dsmmsubg  18774  dsmmlss  18775  islindf2  18849  f1lindf  18857  islindf4  18873  prdstps  20130  qtopval2  20197  tsmsres  20646  climcncf  21404  itg2gt0  22167  ulmval  22775  pserulm  22817  jensen  23318  isismt  23921  iseupa  24965  isgrpoi  25200  isgrp2d  25237  isgrpda  25299  elghomlem2OLD  25364  isrngod  25381  vcoprne  25472  isvc  25474  isnv  25505  cnnvg  25583  cnnvs  25586  cnnvnm  25587  cncph  25734  ajval  25777  hvmulex  25928  hhph  26095  hlimi  26105  chlimi  26152  hhssva  26175  hhsssm  26176  hhssnm  26177  hhshsslem1  26183  elunop  26791  adjeq  26854  leoprf2  27046  fpwrelmapffslem  27555  lmdvg  27935  esumpfinvallem  28080  ofcfval4  28104  omsfval  28265  eulerpartgbij  28311  eulerpartlemmf  28314  sseqval  28327  subfacp1lem5  28628  sinccvglem  29038  elno  29406  mbfresfi  30061  filnetlem4  30199  iscringd  30396  binomcxplemnotnn0  31261  climexp  31611  climinf  31612  limsupre  31647  stirlinglem8  31863  fourierdlem70  31959  fourierdlem71  31960  fourierdlem80  31969  usgra2pth  32354  isassintop  32534  bj-finsumval0  34663  islaut  35807  ispautN  35823  istendo  36486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601
  Copyright terms: Public domain W3C validator