Theorem elfvexd 6900

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450  ‘cfv 6514

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 2702  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-dm 5651  df-iota 6467  df-fv 6522

This theorem is referenced by:  mrieqv2d  17607  mreexmrid  17611  mreexexlem3d  17614  mreexexlem4d  17615  mreexexd  17616  mreexdomd  17617  acsdomd  18523  ismgmn0  18576  ecqusaddcl  19132  telgsumfz  19927  isirred  20335  tgclb  22864  alexsublem  23938  cnextcn  23961  ustssel  24100  fmucnd  24186  trcfilu  24188  cfiluweak  24189  ucnextcn  24198  imasdsf1olem  24268  imasf1oxmet  24270  comet  24408  restmetu  24465  wlkp1lem4  29611  wlkp1lem8  29615  1wlkdlem4  30076  eupth2lem3lem1  30164  eupth2lem3lem2  30165  gsumsubg  32993  opprqusplusg  33467  opprqus0g  33468  lsssra  33591  lbsdiflsp0  33629  fedgmullem1  33632  mzpcl34  42726  xlimbr  45832  xlimmnfvlem2  45838  xlimpnfvlem2  45842  sectpropdlem  49029  invpropdlem  49031  isopropdlem  49033  cicpropdlem  49042  oppcup3  49202  elxpcbasex1ALT  49242  elxpcbasex2ALT  49244  swapf1  49265