Theorem elexd 2699

Description: If a class is a member of another class, it is a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.)

Hypothesis

Ref	Expression
elexd.1	|- ( ph -> A e. V )

Assertion

Ref	Expression
elexd	|- ( ph -> A e. _V )

Proof of Theorem elexd

Step	Hyp	Ref	Expression
1		elexd.1	. 2 |- ( ph -> A e. V )
2		elex 2697	. 2 |- ( A e. V -> A e. _V )
3	1, 2	syl 14	1 |- ( ph -> A e. _V )

Syntax hints:   -> wi 4   e. wcel 1480   _Vcvv 2686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-v 2688

This theorem is referenced by:  dmmptd  5253  tfr1onlemsucfn  6237  tfrcllemsucfn  6250  frecrdg  6305  unsnfidcel  6809  fnfi  6825  caseinl  6976  caseinr  6977  acfun  7063  seq3val  10231  seqvalcd  10232  hashennn  10526  lcmval  11744  hashdvds  11897  ennnfonelemp1  11919  isstruct2r  11970  strnfvnd  11979  strfvssn  11981  strslfv2d  12001  setsslid  12009  ressid2  12018  ressval2  12019  istopon  12180  istps  12199  tgclb  12234  restbasg  12337  restco  12343  lmfval  12361  cnfval  12363  cnpfval  12364  cnpval  12367  txcnp  12440  txrest  12445  ismet2  12523  xmetpsmet  12538  mopnval  12611  comet  12668  reldvg  12817  dvmptclx  12849