Theorem elfvexd 6941

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Vcvv 3454  ‘cfv 6555

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-dm 5665  df-iota 6509  df-fv 6563

This theorem is used by:  mrieqv2d  17839  mreexmrid  17843  mreexexlem3d  17846  mreexexlem4d  17847  mreexexd  17848  mreexdomd  17849  acsmapd  18754  acsdomd  18757  ismgmn0  18844  ecqusaddcl  19434  telgsumfz  20231  isirred  20676  tgclb  23315  alexsublem  24390  cnextcn  24413  ustssel  24552  fmucnd  24637  trcfilu  24639  cfiluweak  24640  ucnextcn  24649  imasdsf1olem  24719  imasf1oxmet  24721  comet  24859  restmetu  24916  wlkp1lem4  30282  wlkp1lem8  30286  1wlkdlem4  30758  eupth2lem3lem1  30856  eupth2lem3lem2  30857  gsumsubg  33674  gsummptfzsplitla  33687  opprqusplusg  34080  opprqus0g  34081  lsssra  34287  lbsdiflsp0  34325  fedgmullem1  34328  mzpcl34  43933  xlimbr  47040  xlimmnfvlem2  47046  xlimpnfvlem2  47050  sectpropdlem  50353  invpropdlem  50355  isopropdlem  50357  cicpropdlem  50366  oppcup3  50528  elxpcbasex1ALT  50574  elxpcbasex2ALT  50576  swapf1  50597