Theorem elfvexd 6866

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

Syntax hints:   → wi 4   ∈ wcel 2121  Vcvv 3433  ‘cfv 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-nul 5230  ax-pr 5364

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-dm 5630  df-iota 6444  df-fv 6496

This theorem is referenced by:  mrieqv2d  17600  mreexmrid  17604  mreexexlem3d  17607  mreexexlem4d  17608  mreexexd  17609  mreexdomd  17610  acsdomd  18518  ismgmn0  18605  ecqusaddcl  19163  telgsumfz  19959  isirred  20393  tgclb  22956  alexsublem  24030  cnextcn  24053  ustssel  24192  fmucnd  24277  trcfilu  24279  cfiluweak  24280  ucnextcn  24289  imasdsf1olem  24359  imasf1oxmet  24361  comet  24499  restmetu  24556  wlkp1lem4  29763  wlkp1lem8  29767  1wlkdlem4  30230  eupth2lem3lem1  30318  eupth2lem3lem2  30319  gsumsubg  33129  gsummptfzsplitla  33142  opprqusplusg  33574  opprqus0g  33575  lsssra  33782  lbsdiflsp0  33820  fedgmullem1  33823  mzpcl34  43193  xlimbr  46282  xlimmnfvlem2  46288  xlimpnfvlem2  46292  sectpropdlem  49538  invpropdlem  49540  isopropdlem  49542  cicpropdlem  49551  oppcup3  49711  elxpcbasex1ALT  49751  elxpcbasex2ALT  49753  swapf1  49774