Theorem elfvexd 6864

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436  ‘cfv 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-dm 5629  df-iota 6443  df-fv 6495

This theorem is referenced by:  mrieqv2d  17551  mreexmrid  17555  mreexexlem3d  17558  mreexexlem4d  17559  mreexexd  17560  mreexdomd  17561  acsdomd  18469  ismgmn0  18556  ecqusaddcl  19111  telgsumfz  19908  isirred  20343  tgclb  22891  alexsublem  23965  cnextcn  23988  ustssel  24127  fmucnd  24212  trcfilu  24214  cfiluweak  24215  ucnextcn  24224  imasdsf1olem  24294  imasf1oxmet  24296  comet  24434  restmetu  24491  wlkp1lem4  29660  wlkp1lem8  29664  1wlkdlem4  30127  eupth2lem3lem1  30215  eupth2lem3lem2  30216  gsumsubg  33033  opprqusplusg  33461  opprqus0g  33462  lsssra  33607  lbsdiflsp0  33646  fedgmullem1  33649  mzpcl34  42829  xlimbr  45930  xlimmnfvlem2  45936  xlimpnfvlem2  45940  sectpropdlem  49142  invpropdlem  49144  isopropdlem  49146  cicpropdlem  49155  oppcup3  49315  elxpcbasex1ALT  49355  elxpcbasex2ALT  49357  swapf1  49378