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

Theorem elfvexd 6179
Description: If a function value is nonempty, its argument is a set. Deduction form of elfvex 6178. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
elfvexd.1 (𝜑𝐴 ∈ (𝐵𝐶))
Assertion
Ref Expression
elfvexd (𝜑𝐶 ∈ V)

Proof of Theorem elfvexd
StepHypRef Expression
1 elfvexd.1 . 2 (𝜑𝐴 ∈ (𝐵𝐶))
2 elfvex 6178 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐶 ∈ V)
31, 2syl 17 1 (𝜑𝐶 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  Vcvv 3186  cfv 5847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4749  ax-pow 4803
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-dm 5084  df-iota 5810  df-fv 5855
This theorem is referenced by:  mrieqv2d  16220  mreexmrid  16224  mreexexlem3d  16227  mreexexlem4d  16228  mreexexd  16229  mreexexdOLD  16230  mreexdomd  16231  acsdomd  17102  ismgmn0  17165  telgsumfz  18308  isirred  18620  tgclb  20685  alexsublem  21758  cnextcn  21781  ustssel  21919  fmucnd  22006  trcfilu  22008  cfiluweak  22009  ucnextcn  22018  imasdsf1olem  22088  imasf1oxmet  22090  comet  22228  restmetu  22285  1loopgredg  26283  1egrvtxdg0  26293  wlkp1lem4  26442  wlkp1lem8  26446  1wlkdlem4  26866  eupth2lem3lem1  26954  eupth2lem3lem2  26955  esumcvg  29926  mzpcl34  36771  dvnprodlem1  39464
  Copyright terms: Public domain W3C validator