Theorem elfvexd 6930

Description: If a function value has a member, then its argument is a set. Deduction form of elfvex 6929. (An artifact of our function value definition.) (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
elfvexd.1	⊢ (𝜑 → 𝐴 ∈ (𝐵‘𝐶))

Assertion

Ref	Expression
elfvexd	⊢ (𝜑 → 𝐶 ∈ V)

Proof of Theorem elfvexd

Step	Hyp	Ref	Expression
1		elfvexd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ (𝐵‘𝐶))
2		elfvex 6929	. 2 ⊢ (𝐴 ∈ (𝐵‘𝐶) → 𝐶 ∈ V)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐶 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3474  ‘cfv 6543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-dm 5686  df-iota 6495  df-fv 6551

This theorem is referenced by:  mrieqv2d  17582  mreexmrid  17586  mreexexlem3d  17589  mreexexlem4d  17590  mreexexd  17591  mreexdomd  17592  acsdomd  18509  ismgmn0  18562  telgsumfz  19857  isirred  20232  tgclb  22472  alexsublem  23547  cnextcn  23570  ustssel  23709  fmucnd  23796  trcfilu  23798  cfiluweak  23799  ucnextcn  23808  imasdsf1olem  23878  imasf1oxmet  23880  comet  24021  restmetu  24078  wlkp1lem4  28930  wlkp1lem8  28934  1wlkdlem4  29390  eupth2lem3lem1  29478  eupth2lem3lem2  29479  gsumsubg  32193  opprqusplusg  32598  opprqus0g  32599  lbsdiflsp0  32706  fedgmullem1  32709  mzpcl34  41459  xlimbr  44533  xlimmnfvlem2  44539  xlimpnfvlem2  44543  ecqusaddcl  46759