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

Theorem elfvex 5893
Description: If a function value has a member, the argument is a set. (Contributed by Mario Carneiro, 6-Nov-2015.)
Assertion
Ref Expression
elfvex  |-  ( A  e.  ( F `  B )  ->  B  e.  _V )

Proof of Theorem elfvex
StepHypRef Expression
1 elfvdm 5892 . 2  |-  ( A  e.  ( F `  B )  ->  B  e.  dom  F )
2 elex 3122 . 2  |-  ( B  e.  dom  F  ->  B  e.  _V )
31, 2syl 16 1  |-  ( A  e.  ( F `  B )  ->  B  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   _Vcvv 3113   dom cdm 4999   ` cfv 5588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-nul 4576  ax-pow 4625
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-dm 5009  df-iota 5551  df-fv 5596
This theorem is referenced by:  elfvexd  5894  fviss  5925  fiin  7882  elharval  7989  elfzp12  11757  ismre  14845  ismri  14886  isacs  14906  oppccofval  14972  gexid  16407  efgrcl  16539  islss  17381  thlle  18523  islbs4  18662  istopon  19221  fgval  20134  fgcl  20142  ufilen  20194  ustssxp  20470  ustbasel  20472  ustincl  20473  ustdiag  20474  ustinvel  20475  ustexhalf  20476  ustfilxp  20478  ustbas2  20491  trust  20495  utopval  20498  elutop  20499  restutop  20503  ustuqtop5  20511  isucn  20544  psmetdmdm  20572  psmetf  20573  psmet0  20575  psmettri2  20576  psmetres2  20581  ismet2  20599  xmetpsmet  20614  metustfbasOLD  20831  metustfbas  20832  metustOLD  20833  metust  20834  iscmet  21486  ulmscl  22536  metidval  27533  pstmval  27538  pstmxmet  27540  issiga  27779  insiga  27805  istotbnd  29896  isbnd  29907  ismrc  30265  isnacs  30268  mzpcl1  30293  mzpcl2  30294  mzpf  30300  mzpadd  30302  mzpmul  30303  mzpsubmpt  30307  mzpnegmpt  30308  mzpexpmpt  30309  mzpindd  30310  mzpsubst  30313  mzpcompact2  30317  mzpcong  30542  clintop  31988  assintop  31989  clintopcllaw  31991  assintopcllaw  31992  assintopass  31994
  Copyright terms: Public domain W3C validator