Theorem elfvexd 6880

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442  ‘cfv 6502

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5255  ax-pr 5381

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-dm 5644  df-iota 6458  df-fv 6510

This theorem is referenced by:  mrieqv2d  17576  mreexmrid  17580  mreexexlem3d  17583  mreexexlem4d  17584  mreexexd  17585  mreexdomd  17586  acsdomd  18494  ismgmn0  18581  ecqusaddcl  19139  telgsumfz  19936  isirred  20372  tgclb  22931  alexsublem  24005  cnextcn  24028  ustssel  24167  fmucnd  24252  trcfilu  24254  cfiluweak  24255  ucnextcn  24264  imasdsf1olem  24334  imasf1oxmet  24336  comet  24474  restmetu  24531  wlkp1lem4  29766  wlkp1lem8  29770  1wlkdlem4  30233  eupth2lem3lem1  30321  eupth2lem3lem2  30322  gsumsubg  33146  gsummptfzsplitla  33159  opprqusplusg  33588  opprqus0g  33589  lsssra  33771  lbsdiflsp0  33810  fedgmullem1  33813  mzpcl34  43117  xlimbr  46214  xlimmnfvlem2  46220  xlimpnfvlem2  46224  sectpropdlem  49424  invpropdlem  49426  isopropdlem  49428  cicpropdlem  49437  oppcup3  49597  elxpcbasex1ALT  49637  elxpcbasex2ALT  49639  swapf1  49660