Theorem elexd 2813

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 2811	. 2 |- ( A e. V -> A e. _V )
3	1, 2	syl 14	1 |- ( ph -> A e. _V )

Syntax hints:   -> wi 4   e. wcel 2200   _Vcvv 2799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2801

This theorem is referenced by:  ifexd  4575  dmmptd  5454  tfr1onlemsucfn  6486  tfrcllemsucfn  6499  frecrdg  6554  unsnfidcel  7083  fnfi  7103  caseinl  7258  caseinr  7259  omniwomnimkv  7334  nninfdcinf  7338  acfun  7389  seq3val  10682  seqvalcd  10683  seqf1oglem2  10742  seqf1og  10743  hashennn  11002  wrdexg  11082  lswex  11123  swrdspsleq  11199  cats1un  11253  cats1fvd  11298  s3fv0g  11323  s3fv1g  11324  lcmval  12585  hashdvds  12743  ennnfonelemp1  12977  isstruct2r  13043  strnfvnd  13052  strfvssn  13054  strslfv2d  13075  setsslid  13083  basmex  13092  basmexd  13093  ressbas2d  13101  ressval3d  13105  prdsex  13302  prdsval  13306  prdsbaslemss  13307  imasival  13339  imasbas  13340  imasplusg  13341  imasmulr  13342  imasaddfn  13350  imasaddval  13351  imasaddf  13352  imasmulfn  13353  imasmulval  13354  imasmulf  13355  qusval  13356  qusaddflemg  13367  qusaddval  13368  qusaddf  13369  qusmulval  13370  qusmulf  13371  xpsfrnel  13377  xpsval  13385  ismgmn0  13391  igsumvalx  13422  gsumfzval  13424  gsumval2  13430  prdssgrpd  13448  ress0g  13476  prdsidlem  13480  prdsmndd  13481  prds0g  13482  ismhm  13494  mhmex  13495  0mhm  13519  prdsgrpd  13642  prdsinvgd  13643  qusgrp2  13650  mulgval  13659  mulgfng  13661  mulg1  13666  mulgnnp1  13667  mulgnndir  13688  issubg2m  13726  1nsgtrivd  13756  eqgval  13760  eqgen  13764  rngpropd  13918  qusrng  13921  issrg  13928  ringidss  13992  ringpropd  14001  qusring2  14029  dvdsrvald  14057  dvdsrd  14058  isunitd  14070  invrfvald  14086  dvrfvald  14097  rdivmuldivd  14108  invrpropdg  14113  isrim0  14125  rhmunitinv  14142  subrgintm  14207  rrgmex  14225  aprval  14246  lssmex  14319  islss3  14343  sraval  14401  sralemg  14402  srascag  14406  sravscag  14407  sraipg  14408  sraex  14410  lidlmex  14439  lidlrsppropdg  14459  2idlmex  14465  qusrhm  14492  zrhval  14581  psrval  14630  psrbasg  14638  psrplusgg  14642  psraddcl  14644  psr0cl  14645  psr0lid  14646  psrnegcl  14647  psrlinv  14648  psrgrp  14649  psr1clfi  14652  mplsubgfilemcl  14663  istopon  14687  istps  14706  tgclb  14739  restbasg  14842  restco  14848  lmfval  14867  cnfval  14868  cnpfval  14869  cnpval  14872  txcnp  14945  txrest  14950  ismet2  15028  xmetpsmet  15043  mopnval  15116  comet  15173  reldvg  15353  dvmptclx  15392  lgseisenlem2  15750  1vgrex  15821  upgriswlkdc  16071