Theorem elfvexd 6929

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

Syntax hints:   → wi 4   ∈ wcel 2104  Vcvv 3472  ‘cfv 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-dm 5685  df-iota 6494  df-fv 6550

This theorem is referenced by:  mrieqv2d  17587  mreexmrid  17591  mreexexlem3d  17594  mreexexlem4d  17595  mreexexd  17596  mreexdomd  17597  acsdomd  18514  ismgmn0  18567  ecqusaddcl  19108  telgsumfz  19899  isirred  20310  tgclb  22693  alexsublem  23768  cnextcn  23791  ustssel  23930  fmucnd  24017  trcfilu  24019  cfiluweak  24020  ucnextcn  24029  imasdsf1olem  24099  imasf1oxmet  24101  comet  24242  restmetu  24299  wlkp1lem4  29200  wlkp1lem8  29204  1wlkdlem4  29660  eupth2lem3lem1  29748  eupth2lem3lem2  29749  gsumsubg  32468  opprqusplusg  32877  opprqus0g  32878  lsssra  32963  lbsdiflsp0  32999  fedgmullem1  33002  mzpcl34  41771  xlimbr  44841  xlimmnfvlem2  44847  xlimpnfvlem2  44851