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 2108  Vcvv 3480  ‘cfv 6561

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-dm 5695  df-iota 6514  df-fv 6569

This theorem is referenced by:  mrieqv2d  17682  mreexmrid  17686  mreexexlem3d  17689  mreexexlem4d  17690  mreexexd  17691  mreexdomd  17692  acsdomd  18602  ismgmn0  18655  ecqusaddcl  19211  telgsumfz  20008  isirred  20419  tgclb  22977  alexsublem  24052  cnextcn  24075  ustssel  24214  fmucnd  24301  trcfilu  24303  cfiluweak  24304  ucnextcn  24313  imasdsf1olem  24383  imasf1oxmet  24385  comet  24526  restmetu  24583  wlkp1lem4  29694  wlkp1lem8  29698  1wlkdlem4  30159  eupth2lem3lem1  30247  eupth2lem3lem2  30248  gsumsubg  33049  opprqusplusg  33517  opprqus0g  33518  lsssra  33639  lbsdiflsp0  33677  fedgmullem1  33680  mzpcl34  42742  xlimbr  45842  xlimmnfvlem2  45848  xlimpnfvlem2  45852  elxpcbasex1ALT  48955  elxpcbasex2ALT  48957  swapf1  48978