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

Theorem elfvex 5717
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 5716 . 2  |-  ( A  e.  ( F `  B )  ->  B  e.  dom  F )
2 elex 2981 . 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 1756   _Vcvv 2972   dom cdm 4840   ` cfv 5418
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-nul 4421  ax-pow 4470
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-dm 4850  df-iota 5381  df-fv 5426
This theorem is referenced by:  elfvexd  5718  fviss  5749  fiin  7672  elharval  7778  elfzp12  11539  ismre  14528  ismri  14569  isacs  14589  oppccofval  14655  gexid  16080  efgrcl  16212  islss  17016  thlle  18122  islbs4  18261  istopon  18530  fgval  19443  fgcl  19451  ufilen  19503  ustssxp  19779  ustbasel  19781  ustincl  19782  ustdiag  19783  ustinvel  19784  ustexhalf  19785  ustfilxp  19787  ustbas2  19800  trust  19804  utopval  19807  elutop  19808  restutop  19812  ustuqtop5  19820  isucn  19853  psmetdmdm  19881  psmetf  19882  psmet0  19884  psmettri2  19885  psmetres2  19890  ismet2  19908  xmetpsmet  19923  metustfbasOLD  20140  metustfbas  20141  metustOLD  20142  metust  20143  iscmet  20795  ulmscl  21844  metidval  26317  pstmval  26322  pstmxmet  26324  issiga  26554  insiga  26580  istotbnd  28668  isbnd  28679  ismrc  29037  isnacs  29040  mzpcl1  29065  mzpcl2  29066  mzpf  29072  mzpadd  29074  mzpmul  29075  mzpsubmpt  29079  mzpnegmpt  29080  mzpexpmpt  29081  mzpindd  29082  mzpsubst  29085  mzpcompact2  29089  mzpcong  29315
  Copyright terms: Public domain W3C validator