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

Theorem elfvexd 5706
Description: If a function value is nonempty, its argument is a set. Deduction form of elfvex 5705. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
elfvexd.1  |-  ( ph  ->  A  e.  ( B `
 C ) )
Assertion
Ref Expression
elfvexd  |-  ( ph  ->  C  e.  _V )

Proof of Theorem elfvexd
StepHypRef Expression
1 elfvexd.1 . 2  |-  ( ph  ->  A  e.  ( B `
 C ) )
2 elfvex 5705 . 2  |-  ( A  e.  ( B `  C )  ->  C  e.  _V )
31, 2syl 16 1  |-  ( ph  ->  C  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   _Vcvv 2962   ` cfv 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-nul 4409  ax-pow 4458
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-dm 4837  df-iota 5369  df-fv 5414
This theorem is referenced by:  mrieqv2d  14559  mreexmrid  14563  mreexexlem3d  14566  mreexexlem4d  14567  mreexexd  14568  mreexdomd  14569  acsdomd  15333  isirred  16724  tgclb  18416  alexsublem  19457  cnextcn  19480  ustssel  19621  fmucnd  19708  trcfilu  19710  cfiluweak  19711  ucnextcn  19720  imasdsf1olem  19789  imasf1oxmet  19791  comet  19929  restmetu  20003  esumcvg  26388  mzpcl34  28909  stoweidlem57  29695
  Copyright terms: Public domain W3C validator