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

Theorem elfvexd 5877
Description: If a function value is nonempty, its argument is a set. Deduction form of elfvex 5876. (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 5876 . 2  |-  ( A  e.  ( B `  C )  ->  C  e.  _V )
31, 2syl 17 1  |-  ( ph  ->  C  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842   _Vcvv 3059   ` cfv 5569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-nul 4525  ax-pow 4572
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-dm 4833  df-iota 5533  df-fv 5577
This theorem is referenced by:  mrieqv2d  15253  mreexmrid  15257  mreexexlem3d  15260  mreexexlem4d  15261  mreexexd  15262  mreexdomd  15263  acsdomd  16135  ismgmn0  16198  telgsumfz  17339  isirred  17668  tgclb  19764  alexsublem  20836  cnextcn  20859  ustssel  21000  fmucnd  21087  trcfilu  21089  cfiluweak  21090  ucnextcn  21099  imasdsf1olem  21168  imasf1oxmet  21170  comet  21308  restmetu  21382  esumcvg  28533  mzpcl34  35025  dvnprodlem1  37111
  Copyright terms: Public domain W3C validator