Theorem elfvexd 6918

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3453  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-dm 5669  df-iota 6493  df-fv 6545

This theorem is used by:  mrieqv2d  17731  mreexmrid  17735  mreexexlem3d  17738  mreexexlem4d  17739  mreexexd  17740  mreexdomd  17741  acsdomd  18649  ismgmn0  18736  ecqusaddcl  19322  telgsumfz  20118  isirred  20561  tgclb  23196  alexsublem  24271  cnextcn  24294  ustssel  24433  fmucnd  24518  trcfilu  24520  cfiluweak  24521  ucnextcn  24530  imasdsf1olem  24600  imasf1oxmet  24602  comet  24740  restmetu  24797  wlkp1lem4  30120  wlkp1lem8  30124  1wlkdlem4  30596  eupth2lem3lem1  30694  eupth2lem3lem2  30695  gsumsubg  33473  gsummptfzsplitla  33486  opprqusplusg  33878  opprqus0g  33879  lsssra  34085  lbsdiflsp0  34123  fedgmullem1  34126  mzpcl34  43563  xlimbr  46642  xlimmnfvlem2  46648  xlimpnfvlem2  46652  sectpropdlem  49949  invpropdlem  49951  isopropdlem  49953  cicpropdlem  49962  oppcup3  50122  elxpcbasex1ALT  50162  elxpcbasex2ALT  50164  swapf1  50185