Theorem elfvexd 6871

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3441  ‘cfv 6493

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 2709  ax-nul 5252  ax-pr 5378

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-dm 5635  df-iota 6449  df-fv 6501

This theorem is referenced by:  mrieqv2d  17567  mreexmrid  17571  mreexexlem3d  17574  mreexexlem4d  17575  mreexexd  17576  mreexdomd  17577  acsdomd  18485  ismgmn0  18572  ecqusaddcl  19127  telgsumfz  19924  isirred  20360  tgclb  22919  alexsublem  23993  cnextcn  24016  ustssel  24155  fmucnd  24240  trcfilu  24242  cfiluweak  24243  ucnextcn  24252  imasdsf1olem  24322  imasf1oxmet  24324  comet  24462  restmetu  24519  wlkp1lem4  29753  wlkp1lem8  29757  1wlkdlem4  30220  eupth2lem3lem1  30308  eupth2lem3lem2  30309  gsumsubg  33132  gsummptfzsplitla  33145  opprqusplusg  33574  opprqus0g  33575  lsssra  33757  lbsdiflsp0  33796  fedgmullem1  33799  mzpcl34  43051  xlimbr  46148  xlimmnfvlem2  46154  xlimpnfvlem2  46158  sectpropdlem  49358  invpropdlem  49360  isopropdlem  49362  cicpropdlem  49371  oppcup3  49531  elxpcbasex1ALT  49571  elxpcbasex2ALT  49573  swapf1  49594