Theorem elfvexd 6845

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3441  ‘cfv 6463

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-nul 5243  ax-pr 5365

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4849  df-br 5086  df-dm 5615  df-iota 6415  df-fv 6471

This theorem is referenced by:  mrieqv2d  17415  mreexmrid  17419  mreexexlem3d  17422  mreexexlem4d  17423  mreexexd  17424  mreexdomd  17425  acsdomd  18342  ismgmn0  18395  telgsumfz  19658  isirred  20008  tgclb  22191  alexsublem  23266  cnextcn  23289  ustssel  23428  fmucnd  23515  trcfilu  23517  cfiluweak  23518  ucnextcn  23527  imasdsf1olem  23597  imasf1oxmet  23599  comet  23740  restmetu  23797  wlkp1lem4  28152  wlkp1lem8  28156  1wlkdlem4  28612  eupth2lem3lem1  28700  eupth2lem3lem2  28701  gsumsubg  31414  lbsdiflsp0  31813  fedgmullem1  31816  mzpcl34  40763  xlimbr  43612  xlimmnfvlem2  43618  xlimpnfvlem2  43622