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  6492  tfrcllemsucfn  6505  frecrdg  6560  unsnfidcel  7091  fnfi  7111  caseinl  7266  caseinr  7267  omniwomnimkv  7342  nninfdcinf  7346  acfun  7397  seq3val  10690  seqvalcd  10691  seqf1oglem2  10750  seqf1og  10751  hashennn  11010  wrdexg  11090  lswex  11131  swrdspsleq  11207  cats1un  11261  cats1fvd  11306  s3fv0g  11331  s3fv1g  11332  lcmval  12593  hashdvds  12751  ennnfonelemp1  12985  isstruct2r  13051  strnfvnd  13060  strfvssn  13062  strslfv2d  13083  setsslid  13091  basmex  13100  basmexd  13101  ressbas2d  13109  ressval3d  13113  prdsex  13310  prdsval  13314  prdsbaslemss  13315  imasival  13347  imasbas  13348  imasplusg  13349  imasmulr  13350  imasaddfn  13358  imasaddval  13359  imasaddf  13360  imasmulfn  13361  imasmulval  13362  imasmulf  13363  qusval  13364  qusaddflemg  13375  qusaddval  13376  qusaddf  13377  qusmulval  13378  qusmulf  13379  xpsfrnel  13385  xpsval  13393  ismgmn0  13399  igsumvalx  13430  gsumfzval  13432  gsumval2  13438  prdssgrpd  13456  ress0g  13484  prdsidlem  13488  prdsmndd  13489  prds0g  13490  ismhm  13502  mhmex  13503  0mhm  13527  prdsgrpd  13650  prdsinvgd  13651  qusgrp2  13658  mulgval  13667  mulgfng  13669  mulg1  13674  mulgnnp1  13675  mulgnndir  13696  issubg2m  13734  1nsgtrivd  13764  eqgval  13768  eqgen  13772  rngpropd  13926  qusrng  13929  issrg  13936  ringidss  14000  ringpropd  14009  qusring2  14037  dvdsrvald  14065  dvdsrd  14066  isunitd  14078  invrfvald  14094  dvrfvald  14105  rdivmuldivd  14116  invrpropdg  14121  isrim0  14133  rhmunitinv  14150  subrgintm  14215  rrgmex  14233  aprval  14254  lssmex  14327  islss3  14351  sraval  14409  sralemg  14410  srascag  14414  sravscag  14415  sraipg  14416  sraex  14418  lidlmex  14447  lidlrsppropdg  14467  2idlmex  14473  qusrhm  14500  zrhval  14589  psrval  14638  psrbasg  14646  psrplusgg  14650  psraddcl  14652  psr0cl  14653  psr0lid  14654  psrnegcl  14655  psrlinv  14656  psrgrp  14657  psr1clfi  14660  mplsubgfilemcl  14671  istopon  14695  istps  14714  tgclb  14747  restbasg  14850  restco  14856  lmfval  14875  cnfval  14876  cnpfval  14877  cnpval  14880  txcnp  14953  txrest  14958  ismet2  15036  xmetpsmet  15051  mopnval  15124  comet  15181  reldvg  15361  dvmptclx  15400  lgseisenlem2  15758  1vgrex  15829  upgriswlkdc  16081