Theorem elfvexd 6945

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3477  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-dm 5698  df-iota 6515  df-fv 6570

This theorem is referenced by:  mrieqv2d  17683  mreexmrid  17687  mreexexlem3d  17690  mreexexlem4d  17691  mreexexd  17692  mreexdomd  17693  acsdomd  18614  ismgmn0  18667  ecqusaddcl  19223  telgsumfz  20022  isirred  20435  tgclb  22992  alexsublem  24067  cnextcn  24090  ustssel  24229  fmucnd  24316  trcfilu  24318  cfiluweak  24319  ucnextcn  24328  imasdsf1olem  24398  imasf1oxmet  24400  comet  24541  restmetu  24598  wlkp1lem4  29708  wlkp1lem8  29712  1wlkdlem4  30168  eupth2lem3lem1  30256  eupth2lem3lem2  30257  gsumsubg  33031  opprqusplusg  33496  opprqus0g  33497  lsssra  33617  lbsdiflsp0  33653  fedgmullem1  33656  mzpcl34  42718  xlimbr  45782  xlimmnfvlem2  45788  xlimpnfvlem2  45792