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

Theorem fex 6369
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
StepHypRef Expression
1 ffn 5941 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnex 6361 . 2 ((𝐹 Fn 𝐴𝐴𝐶) → 𝐹 ∈ V)
31, 2sylan 486 1 ((𝐹:𝐴𝐵𝐴𝐶) → 𝐹 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  Vcvv 3169   Fn wfn 5782  wf 5783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pr 4825
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-reu 2899  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-id 4940  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795
This theorem is referenced by:  f1oexrnex  6982  frnsuppeq  7168  suppsnop  7170  f1domg  7835  fdmfisuppfi  8141  frnfsuppbi  8161  fsuppco2  8165  fsuppcor  8166  mapfienlem2  8168  ordtypelem10  8289  oiexg  8297  cnfcom3clem  8459  infxpenc2lem2  8700  fin23lem32  9023  isf32lem10  9041  focdmex  12950  hasheqf1oi  12951  hashf1rn  12953  hashf1rnOLD  12954  hasheqf1od  12955  hashimarn  13034  hashf1lem1  13045  fz1isolem  13051  iswrd  13105  climsup  14191  fsum  14241  supcvg  14370  fprod  14453  vdwmc  15463  vdwpc  15465  ramval  15493  imasval  15937  imasle  15949  pwsco1mhm  17136  isghm  17426  elsymgbas  17568  gsumval3a  18070  gsumval3lem1  18072  gsumval3lem2  18073  gsumzres  18076  gsumzf1o  18079  gsumzaddlem  18087  gsumzadd  18088  gsumzmhm  18103  gsumzoppg  18110  gsumpt  18127  gsum2dlem2  18136  dmdprd  18163  prdslmodd  18733  gsumply1subr  19368  dsmmsubg  19845  dsmmlss  19846  islindf2  19911  f1lindf  19919  islindf4  19935  prdstps  21181  qtopval2  21248  tsmsres  21696  climcncf  22439  itg2gt0  23247  ulmval  23852  pserulm  23894  jensen  24429  isismt  25144  iseupa  26255  isgrpoi  26499  vcoprneOLD  26597  isvcOLD  26599  isnv  26632  cnnvg  26710  cnnvs  26713  cnnvnm  26714  cncph  26861  ajval  26904  hvmulex  27055  hhph  27222  hlimi  27232  chlimi  27278  hhssva  27301  hhsssm  27302  hhssnm  27303  hhshsslem1  27311  elunop  27918  adjeq  27981  leoprf2  28173  fpwrelmapffslem  28698  lmdvg  29130  esumpfinvallem  29266  ofcfval4  29297  omsfval  29486  omsf  29488  omssubadd  29492  carsgval  29495  eulerpartgbij  29564  eulerpartlemmf  29567  sseqval  29580  subfacp1lem5  30223  sinccvglem  30623  elno  30846  filnetlem4  31349  bj-finsumval0  32124  poimirlem24  32403  mbfresfi  32426  elghomlem2OLD  32655  isrngod  32667  isgrpda  32724  iscringd  32767  islaut  34187  ispautN  34203  istendo  34866  binomcxplemnotnn0  37377  fexd  38127  fidmfisupp  38185  climexp  38473  climinf  38474  limsupre  38509  stirlinglem8  38775  fourierdlem70  38870  fourierdlem71  38871  fourierdlem80  38880  sge0val  39060  sge0f1o  39076  ismea  39145  meadjiunlem  39159  isomennd  39222  usgr2pth  40969  isassintop  41635  fdivmpt  42131  elbigolo1  42148
  Copyright terms: Public domain W3C validator