Theorem elfvexd 6879

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444  ‘cfv 6499

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-dm 5641  df-iota 6452  df-fv 6507

This theorem is referenced by:  mrieqv2d  17581  mreexmrid  17585  mreexexlem3d  17588  mreexexlem4d  17589  mreexexd  17590  mreexdomd  17591  acsdomd  18499  ismgmn0  18552  ecqusaddcl  19108  telgsumfz  19905  isirred  20340  tgclb  22891  alexsublem  23965  cnextcn  23988  ustssel  24127  fmucnd  24213  trcfilu  24215  cfiluweak  24216  ucnextcn  24225  imasdsf1olem  24295  imasf1oxmet  24297  comet  24435  restmetu  24492  wlkp1lem4  29656  wlkp1lem8  29660  1wlkdlem4  30120  eupth2lem3lem1  30208  eupth2lem3lem2  30209  gsumsubg  33030  opprqusplusg  33454  opprqus0g  33455  lsssra  33578  lbsdiflsp0  33616  fedgmullem1  33619  mzpcl34  42713  xlimbr  45819  xlimmnfvlem2  45825  xlimpnfvlem2  45829  sectpropdlem  49019  invpropdlem  49021  isopropdlem  49023  cicpropdlem  49032  oppcup3  49192  elxpcbasex1ALT  49232  elxpcbasex2ALT  49234  swapf1  49255