Theorem elfvexd 6915

Description: If a function value has a member, then its argument is a set. Deduction form of elfvex 6914. (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 6914	. 2 ⊢ (𝐴 ∈ (𝐵‘𝐶) → 𝐶 ∈ V)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝐶 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3463  ‘cfv 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-nul 5268  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-dm 5669  df-iota 6490  df-fv 6542

This theorem is referenced by:  mrieqv2d  17691  mreexmrid  17695  mreexexlem3d  17698  mreexexlem4d  17699  mreexexd  17700  mreexdomd  17701  acsdomd  18609  ismgmn0  18696  ecqusaddcl  19260  telgsumfz  20056  isirred  20497  tgclb  23092  alexsublem  24166  cnextcn  24189  ustssel  24328  fmucnd  24413  trcfilu  24415  cfiluweak  24416  ucnextcn  24425  imasdsf1olem  24495  imasf1oxmet  24497  comet  24635  restmetu  24692  wlkp1lem4  29961  wlkp1lem8  29965  1wlkdlem4  30428  eupth2lem3lem1  30516  eupth2lem3lem2  30517  gsumsubg  33303  gsummptfzsplitla  33316  opprqusplusg  33712  opprqus0g  33713  lsssra  33919  lbsdiflsp0  33957  fedgmullem1  33960  mzpcl34  43349  xlimbr  46428  xlimmnfvlem2  46434  xlimpnfvlem2  46438  sectpropdlem  49694  invpropdlem  49696  isopropdlem  49698  cicpropdlem  49707  oppcup3  49867  elxpcbasex1ALT  49907  elxpcbasex2ALT  49909  swapf1  49930