Theorem elfvexd 6909

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450  ‘cfv 6527

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-dm 5657  df-iota 6483  df-fv 6535

This theorem is used by:  mrieqv2d  17774  mreexmrid  17778  mreexexlem3d  17781  mreexexlem4d  17782  mreexexd  17783  mreexdomd  17784  acsdomd  18692  ismgmn0  18779  ecqusaddcl  19369  telgsumfz  20165  isirred  20610  tgclb  23249  alexsublem  24324  cnextcn  24347  ustssel  24486  fmucnd  24571  trcfilu  24573  cfiluweak  24574  ucnextcn  24583  imasdsf1olem  24653  imasf1oxmet  24655  comet  24793  restmetu  24850  wlkp1lem4  30188  wlkp1lem8  30192  1wlkdlem4  30664  eupth2lem3lem1  30762  eupth2lem3lem2  30763  gsumsubg  33540  gsummptfzsplitla  33553  opprqusplusg  33946  opprqus0g  33947  lsssra  34153  lbsdiflsp0  34191  fedgmullem1  34194  mzpcl34  43680  xlimbr  46759  xlimmnfvlem2  46765  xlimpnfvlem2  46769  sectpropdlem  50066  invpropdlem  50068  isopropdlem  50070  cicpropdlem  50079  oppcup3  50239  elxpcbasex1ALT  50279  elxpcbasex2ALT  50281  swapf1  50302