Theorem elfvexd 6917

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  Vcvv 3454  ‘cfv 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5268  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-dm 5670  df-iota 6492  df-fv 6544

This theorem is used by:  mrieqv2d  17701  mreexmrid  17705  mreexexlem3d  17708  mreexexlem4d  17709  mreexexd  17710  mreexdomd  17711  acsdomd  18619  ismgmn0  18706  ecqusaddcl  19270  telgsumfz  20066  isirred  20508  tgclb  23138  alexsublem  24212  cnextcn  24235  ustssel  24374  fmucnd  24459  trcfilu  24461  cfiluweak  24462  ucnextcn  24471  imasdsf1olem  24541  imasf1oxmet  24543  comet  24681  restmetu  24738  wlkp1lem4  30035  wlkp1lem8  30039  1wlkdlem4  30502  eupth2lem3lem1  30590  eupth2lem3lem2  30591  gsumsubg  33375  gsummptfzsplitla  33388  opprqusplusg  33780  opprqus0g  33781  lsssra  33987  lbsdiflsp0  34025  fedgmullem1  34028  mzpcl34  43490  xlimbr  46569  xlimmnfvlem2  46575  xlimpnfvlem2  46579  sectpropdlem  49842  invpropdlem  49844  isopropdlem  49846  cicpropdlem  49855  oppcup3  50015  elxpcbasex1ALT  50055  elxpcbasex2ALT  50057  swapf1  50078