Theorem elfvexd 6921

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  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 1572  df-fal 1582  df-ex 1812  df-sb 2099  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-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-dm 5660  df-iota 6494  df-fv 6546

This theorem is used by:  mrieqv2d  17813  mreexmrid  17817  mreexexlem3d  17820  mreexexlem4d  17821  mreexexd  17822  mreexdomd  17823  acsdomd  18731  ismgmn0  18818  ecqusaddcl  19408  telgsumfz  20204  isirred  20649  tgclb  23288  alexsublem  24363  cnextcn  24386  ustssel  24525  fmucnd  24610  trcfilu  24612  cfiluweak  24613  ucnextcn  24622  imasdsf1olem  24692  imasf1oxmet  24694  comet  24832  restmetu  24889  wlkp1lem4  30255  wlkp1lem8  30259  1wlkdlem4  30731  eupth2lem3lem1  30829  eupth2lem3lem2  30830  gsumsubg  33607  gsummptfzsplitla  33620  opprqusplusg  34013  opprqus0g  34014  lsssra  34220  lbsdiflsp0  34258  fedgmullem1  34261  mzpcl34  43742  xlimbr  46837  xlimmnfvlem2  46843  xlimpnfvlem2  46847  sectpropdlem  50144  invpropdlem  50146  isopropdlem  50148  cicpropdlem  50157  oppcup3  50317  elxpcbasex1ALT  50357  elxpcbasex2ALT  50359  swapf1  50380