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

Theorem elfvexd 6375
Description: If a function value is nonempty, its argument is a set. Deduction form of elfvex 6374. (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 6374 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐶 ∈ V)
31, 2syl 17 1 (𝜑𝐶 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2131  Vcvv 3332  cfv 6041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-nul 4933  ax-pow 4984
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-dm 5268  df-iota 6004  df-fv 6049
This theorem is referenced by:  mrieqv2d  16493  mreexmrid  16497  mreexexlem3d  16500  mreexexlem4d  16501  mreexexd  16502  mreexdomd  16503  acsdomd  17374  ismgmn0  17437  telgsumfz  18579  isirred  18891  tgclb  20968  alexsublem  22041  cnextcn  22064  ustssel  22202  fmucnd  22289  trcfilu  22291  cfiluweak  22292  ucnextcn  22301  imasdsf1olem  22371  imasf1oxmet  22373  comet  22511  restmetu  22568  wlkp1lem4  26775  wlkp1lem8  26779  1wlkdlem4  27284  eupth2lem3lem1  27372  eupth2lem3lem2  27373  mzpcl34  37788  xlimbr  40548  xlimmnfvlem2  40554  xlimpnfvlem2  40558
  Copyright terms: Public domain W3C validator