Theorem elfvexd 6905

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

Syntax hints:   → wi 4   ∈ wcel 2144  Vcvv 3456  ‘cfv 6523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-nul 5258  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-dm 5659  df-iota 6479  df-fv 6531

This theorem is referenced by:  mrieqv2d  17673  mreexmrid  17677  mreexexlem3d  17680  mreexexlem4d  17681  mreexexd  17682  mreexdomd  17683  acsdomd  18591  ismgmn0  18678  ecqusaddcl  19236  telgsumfz  20032  isirred  20470  tgclb  23032  alexsublem  24106  cnextcn  24129  ustssel  24268  fmucnd  24353  trcfilu  24355  cfiluweak  24356  ucnextcn  24365  imasdsf1olem  24435  imasf1oxmet  24437  comet  24575  restmetu  24632  wlkp1lem4  29877  wlkp1lem8  29881  1wlkdlem4  30344  eupth2lem3lem1  30432  eupth2lem3lem2  30433  gsumsubg  33228  gsummptfzsplitla  33241  opprqusplusg  33679  opprqus0g  33680  lsssra  33887  lbsdiflsp0  33925  fedgmullem1  33928  mzpcl34  43317  xlimbr  46406  xlimmnfvlem2  46412  xlimpnfvlem2  46416  sectpropdlem  49662  invpropdlem  49664  isopropdlem  49666  cicpropdlem  49675  oppcup3  49835  elxpcbasex1ALT  49875  elxpcbasex2ALT  49877  swapf1  49898