Theorem elfvexd 6859

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3436  ‘cfv 6482

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 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-dm 5629  df-iota 6438  df-fv 6490

This theorem is referenced by:  mrieqv2d  17545  mreexmrid  17549  mreexexlem3d  17552  mreexexlem4d  17553  mreexexd  17554  mreexdomd  17555  acsdomd  18463  ismgmn0  18516  ecqusaddcl  19072  telgsumfz  19869  isirred  20304  tgclb  22855  alexsublem  23929  cnextcn  23952  ustssel  24091  fmucnd  24177  trcfilu  24179  cfiluweak  24180  ucnextcn  24189  imasdsf1olem  24259  imasf1oxmet  24261  comet  24399  restmetu  24456  wlkp1lem4  29624  wlkp1lem8  29628  1wlkdlem4  30088  eupth2lem3lem1  30176  eupth2lem3lem2  30177  gsumsubg  33008  opprqusplusg  33435  opprqus0g  33436  lsssra  33570  lbsdiflsp0  33609  fedgmullem1  33612  mzpcl34  42724  xlimbr  45828  xlimmnfvlem2  45834  xlimpnfvlem2  45838  sectpropdlem  49041  invpropdlem  49043  isopropdlem  49045  cicpropdlem  49054  oppcup3  49214  elxpcbasex1ALT  49254  elxpcbasex2ALT  49256  swapf1  49277