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

Theorem elfvex 5875
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 5874 . 2  |-  ( A  e.  ( F `  B )  ->  B  e.  dom  F )
2 elex 3115 . 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 1823   _Vcvv 3106   dom cdm 4988   ` cfv 5570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-nul 4568  ax-pow 4615
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-dm 4998  df-iota 5534  df-fv 5578
This theorem is referenced by:  elfvexd  5876  fviss  5906  fiin  7874  elharval  7981  elfzp12  11761  ismre  15079  ismri  15120  isacs  15140  oppccofval  15204  gexid  16800  efgrcl  16932  islss  17776  thlle  18901  islbs4  19034  istopon  19593  fgval  20537  fgcl  20545  ufilen  20597  ustssxp  20873  ustbasel  20875  ustincl  20876  ustdiag  20877  ustinvel  20878  ustexhalf  20879  ustfilxp  20881  ustbas2  20894  trust  20898  utopval  20901  elutop  20902  restutop  20906  ustuqtop5  20914  isucn  20947  psmetdmdm  20975  psmetf  20976  psmet0  20978  psmettri2  20979  psmetres2  20984  ismet2  21002  xmetpsmet  21017  metustfbasOLD  21234  metustfbas  21235  metustOLD  21236  metust  21237  iscmet  21889  ulmscl  22940  metidval  28104  pstmval  28109  pstmxmet  28111  issiga  28341  insiga  28367  mvrsval  29129  mrsubcv  29134  mrsubccat  29142  mppsval  29196  istotbnd  30505  isbnd  30516  ismrc  30873  isnacs  30876  mzpcl1  30901  mzpcl2  30902  mzpf  30908  mzpadd  30910  mzpmul  30911  mzpsubmpt  30915  mzpnegmpt  30916  mzpexpmpt  30917  mzpindd  30918  mzpsubst  30920  mzpcompact2  30924  mzpcong  31149  clintop  32904  assintop  32905  clintopcllaw  32907  assintopcllaw  32908  assintopass  32910
  Copyright terms: Public domain W3C validator