Theorem elfvexd 6865

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3427  ‘cfv 6487

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-nul 5230  ax-pr 5364

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-ne 2931  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-ss 3902  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 6443  df-fv 6495

This theorem is referenced by:  mrieqv2d  17594  mreexmrid  17598  mreexexlem3d  17601  mreexexlem4d  17602  mreexexd  17603  mreexdomd  17604  acsdomd  18512  ismgmn0  18599  ecqusaddcl  19157  telgsumfz  19954  isirred  20388  tgclb  22923  alexsublem  23997  cnextcn  24020  ustssel  24159  fmucnd  24244  trcfilu  24246  cfiluweak  24247  ucnextcn  24256  imasdsf1olem  24326  imasf1oxmet  24328  comet  24466  restmetu  24523  wlkp1lem4  29731  wlkp1lem8  29735  1wlkdlem4  30198  eupth2lem3lem1  30286  eupth2lem3lem2  30287  gsumsubg  33095  gsummptfzsplitla  33108  opprqusplusg  33537  opprqus0g  33538  lsssra  33720  lbsdiflsp0  33758  fedgmullem1  33761  mzpcl34  43151  xlimbr  46243  xlimmnfvlem2  46249  xlimpnfvlem2  46253  sectpropdlem  49499  invpropdlem  49501  isopropdlem  49503  cicpropdlem  49512  oppcup3  49672  elxpcbasex1ALT  49712  elxpcbasex2ALT  49714  swapf1  49735