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

Theorem elfvex 5555
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 5554 . 2  |-  ( A  e.  ( F `  B )  ->  B  e.  dom  F )
2 elex 2796 . 2  |-  ( B  e.  dom  F  ->  B  e.  _V )
31, 2syl 15 1  |-  ( A  e.  ( F `  B )  ->  B  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   _Vcvv 2788   dom cdm 4689   ` cfv 5255
This theorem is referenced by:  elfvexd  5556  fviss  5580  fiin  7175  elharval  7277  elfzp12  10861  ismre  13492  ismri  13533  isacs  13553  oppccofval  13619  gexid  14892  efgrcl  15024  islss  15692  thlle  16597  istopon  16663  fgval  17565  fgcl  17573  ufilen  17625  ismet2  17898  iscmet  18710  ulmscl  19758  issiga  23472  insiga  23498  clscnc  26010  istotbnd  26493  isbnd  26504  ismrc  26776  isnacs  26779  mzpcl1  26807  mzpcl2  26808  mzpf  26814  mzpadd  26816  mzpmul  26817  mzpsubmpt  26821  mzpnegmpt  26822  mzpexpmpt  26823  mzpindd  26824  mzpsubst  26826  mzpcompact2  26830  mzpcong  27059  islbs4  27302
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-nul 4149  ax-pow 4188
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-dm 4699  df-iota 5219  df-fv 5263
  Copyright terms: Public domain W3C validator