Theorem elexd 2816

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

Syntax hints:   -> wi 4   e. wcel 2202   _Vcvv 2802

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2804

This theorem is referenced by:  ifexd  4581  dmmptd  5463  tfr1onlemsucfn  6506  tfrcllemsucfn  6519  frecrdg  6574  unsnfidcel  7113  fnfi  7135  caseinl  7290  caseinr  7291  omniwomnimkv  7366  nninfdcinf  7370  acfun  7422  seq3val  10723  seqvalcd  10724  seqf1oglem2  10783  seqf1og  10784  hashennn  11043  wrdexg  11128  lswex  11169  ccatw2s1leng  11219  ccat2s1fvwd  11228  swrdspsleq  11252  cats1un  11306  cats1fvd  11351  s3fv0g  11376  s3fv1g  11377  s3fv2g  11378  s1s3d  11380  s1s4d  11381  s1s5d  11382  s1s6d  11383  s1s7d  11384  s2s2d  11385  s4s2d  11386  s4s3d  11387  s3s4d  11388  s2s5d  11389  s5s2d  11390  s4s4d  11391  lcmval  12653  hashdvds  12811  ennnfonelemp1  13045  isstruct2r  13111  strnfvnd  13120  strfvssn  13122  strslfv2d  13143  setsslid  13151  basmex  13160  basmexd  13161  ressbas2d  13169  ressval3d  13173  prdsex  13370  prdsval  13374  prdsbaslemss  13375  imasival  13407  imasbas  13408  imasplusg  13409  imasmulr  13410  imasaddfn  13418  imasaddval  13419  imasaddf  13420  imasmulfn  13421  imasmulval  13422  imasmulf  13423  qusval  13424  qusaddflemg  13435  qusaddval  13436  qusaddf  13437  qusmulval  13438  qusmulf  13439  xpsfrnel  13445  xpsval  13453  ismgmn0  13459  igsumvalx  13490  gsumfzval  13492  gsumval2  13498  prdssgrpd  13516  ress0g  13544  prdsidlem  13548  prdsmndd  13549  prds0g  13550  ismhm  13562  mhmex  13563  0mhm  13587  prdsgrpd  13710  prdsinvgd  13711  qusgrp2  13718  mulgval  13727  mulgfng  13729  mulg1  13734  mulgnnp1  13735  mulgnndir  13756  issubg2m  13794  1nsgtrivd  13824  eqgval  13828  eqgen  13832  rngpropd  13987  qusrng  13990  issrg  13997  ringidss  14061  ringpropd  14070  qusring2  14098  dvdsrvald  14126  dvdsrd  14127  isunitd  14139  invrfvald  14155  dvrfvald  14166  rdivmuldivd  14177  invrpropdg  14182  isrim0  14194  rhmunitinv  14211  subrgintm  14276  rrgmex  14294  aprval  14315  lssmex  14388  islss3  14412  sraval  14470  sralemg  14471  srascag  14475  sravscag  14476  sraipg  14477  sraex  14479  lidlmex  14508  lidlrsppropdg  14528  2idlmex  14534  qusrhm  14561  zrhval  14650  psrval  14699  psrbasg  14707  psrplusgg  14711  psraddcl  14713  psr0cl  14714  psr0lid  14715  psrnegcl  14716  psrlinv  14717  psrgrp  14718  psr1clfi  14721  mplsubgfilemcl  14732  istopon  14756  istps  14775  tgclb  14808  restbasg  14911  restco  14917  lmfval  14936  cnfval  14937  cnpfval  14938  cnpval  14941  txcnp  15014  txrest  15019  ismet2  15097  xmetpsmet  15112  mopnval  15185  comet  15242  reldvg  15422  dvmptclx  15461  lgseisenlem2  15819  1vgrex  15890  p1evtxdeqfilem  16181  p1evtxdeqfi  16182  p1evtxdp1fi  16183  upgriswlkdc  16230  eupth2lem3fi  16346  eupth2lembfi  16347  gfsumval  16732