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  17580  mreexmrid  17584  mreexexlem3d  17587  mreexexlem4d  17588  mreexexd  17589  mreexdomd  17590  acsdomd  18498  ismgmn0  18551  ecqusaddcl  19107  telgsumfz  19904  isirred  20339  tgclb  22890  alexsublem  23964  cnextcn  23987  ustssel  24126  fmucnd  24212  trcfilu  24214  cfiluweak  24215  ucnextcn  24224  imasdsf1olem  24294  imasf1oxmet  24296  comet  24434  restmetu  24491  wlkp1lem4  29655  wlkp1lem8  29659  1wlkdlem4  30119  eupth2lem3lem1  30207  eupth2lem3lem2  30208  gsumsubg  33029  opprqusplusg  33453  opprqus0g  33454  lsssra  33577  lbsdiflsp0  33615  fedgmullem1  33618  mzpcl34  42712  xlimbr  45818  xlimmnfvlem2  45824  xlimpnfvlem2  45828  sectpropdlem  49018  invpropdlem  49020  isopropdlem  49022  cicpropdlem  49031  oppcup3  49191  elxpcbasex1ALT  49231  elxpcbasex2ALT  49233  swapf1  49254