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

Theorem fex 6977
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 6502 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnex 6968 . 2 ((𝐹 Fn 𝐴𝐴𝐶) → 𝐹 ∈ V)
31, 2sylan 583 1 ((𝐹:𝐴𝐵𝐴𝐶) → 𝐹 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2115  Vcvv 3480   Fn wfn 6338  wf 6339
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pr 5317
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4276  df-if 4450  df-sn 4550  df-pr 4552  df-op 4556  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351
This theorem is referenced by:  fexd  6978  f1oexrnex  7622  frnsuppeq  7832  suppsnop  7834  f1domg  8519  fdmfisuppfi  8833  frnfsuppbi  8853  fsuppco2  8857  fsuppcor  8858  mapfienlem2  8860  ordtypelem10  8982  oiexg  8990  cnfcom3clem  9159  infxpenc2lem2  9438  fin23lem32  9758  isf32lem10  9776  focdmex  13712  hasheqf1oi  13713  hashf1rn  13714  hasheqf1od  13715  hashimarn  13802  hashf1lem1  13814  fz1isolem  13820  iswrd  13864  climsup  15022  fsum  15073  supcvg  15207  fprod  15291  vdwmc  16308  vdwpc  16310  ramval  16338  imasval  16780  imasle  16792  pwsco1mhm  17992  isghm  18354  elsymgbas  18498  gsumval3a  19019  gsumval3lem1  19021  gsumval3lem2  19022  gsumzres  19025  gsumzf1o  19028  gsumzaddlem  19037  gsumzadd  19038  gsumzmhm  19053  gsumzoppg  19060  gsumpt  19078  gsum2dlem2  19087  dmdprd  19116  prdslmodd  19734  gsumply1subr  20395  cnfldfun  20550  cnfldfunALT  20551  dsmmsubg  20880  dsmmlss  20881  islindf2  20951  f1lindf  20959  islindf4  20975  prdstps  22230  qtopval2  22297  tsmsres  22745  tngngp3  23258  climcncf  23501  ulmval  24971  pserulm  25013  jensen  25570  isismt  26324  isgrpoi  28277  isvcOLD  28358  isnv  28391  cnnvg  28457  cnnvs  28459  cnnvnm  28460  cncph  28598  ajval  28640  hvmulex  28790  hhph  28957  hlimi  28967  chlimi  29013  hhssva  29036  hhsssm  29037  hhssnm  29038  hhshsslem1  29046  elunop  29651  adjeq  29714  leoprf2  29906  fpwrelmapffslem  30472  pwrssmgc  30684  lmdvg  31221  esumpfinvallem  31358  ofcfval4  31389  omsfval  31577  omsf  31579  omssubadd  31583  carsgval  31586  eulerpartgbij  31655  eulerpartlemmf  31658  sseqval  31671  subfacp1lem5  32456  sinccvglem  32940  elno  33178  filnetlem4  33754  bj-finsumval0  34613  poimirlem24  34991  mbfresfi  35013  elghomlem2OLD  35234  isrngod  35246  isgrpda  35303  iscringd  35346  islaut  37289  ispautN  37305  istendo  37966  binomcxplemnotnn0  40917  fidmfisupp  41690  climexp  42110  climinf  42111  limsupre  42146  stirlinglem8  42586  fourierdlem70  42681  fourierdlem71  42682  fourierdlem80  42691  sge0val  42868  sge0f1o  42884  ismea  42953  meadjiunlem  42967  isomennd  43033  isassintop  44333  fdivmpt  44816  elbigolo1  44833
  Copyright terms: Public domain W3C validator