Theorem elexd 2817

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 2815	. 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 2803

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  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 2805

This theorem is referenced by:  ifexd  4587  dmmptd  5470  mptsuppd  6434  suppssfvg  6441  tfr1onlemsucfn  6549  tfrcllemsucfn  6562  frecrdg  6617  unsnfidcel  7156  fnfi  7178  caseinl  7350  caseinr  7351  omniwomnimkv  7426  nninfdcinf  7430  acfun  7482  seq3val  10785  seqvalcd  10786  seqf1oglem2  10845  seqf1og  10846  hashennn  11105  wrdexg  11190  lswex  11231  ccatw2s1leng  11281  ccat2s1fvwd  11290  swrdspsleq  11314  cats1un  11368  cats1fvd  11413  s3fv0g  11438  s3fv1g  11439  s3fv2g  11440  s1s3d  11442  s1s4d  11443  s1s5d  11444  s1s6d  11445  s1s7d  11446  s2s2d  11447  s4s2d  11448  s4s3d  11449  s3s4d  11450  s2s5d  11451  s5s2d  11452  s4s4d  11453  lcmval  12715  hashdvds  12873  ennnfonelemp1  13107  isstruct2r  13173  strnfvnd  13182  strfvssn  13184  strslfv2d  13205  setsslid  13213  basmex  13222  basmexd  13223  ressbas2d  13231  ressval3d  13235  prdsex  13432  prdsval  13436  prdsbaslemss  13437  imasival  13469  imasbas  13470  imasplusg  13471  imasmulr  13472  imasaddfn  13480  imasaddval  13481  imasaddf  13482  imasmulfn  13483  imasmulval  13484  imasmulf  13485  qusval  13486  qusaddflemg  13497  qusaddval  13498  qusaddf  13499  qusmulval  13500  qusmulf  13501  xpsfrnel  13507  xpsval  13515  ismgmn0  13521  igsumvalx  13552  gsumfzval  13554  gsumval2  13560  prdssgrpd  13578  ress0g  13606  prdsidlem  13610  prdsmndd  13611  prds0g  13612  ismhm  13624  mhmex  13625  0mhm  13649  prdsgrpd  13772  prdsinvgd  13773  qusgrp2  13780  mulgval  13789  mulgfng  13791  mulg1  13796  mulgnnp1  13797  mulgnndir  13818  issubg2m  13856  1nsgtrivd  13886  eqgval  13890  eqgen  13894  rngpropd  14049  qusrng  14052  issrg  14059  ringidss  14123  ringpropd  14132  qusring2  14160  dvdsrvald  14188  dvdsrd  14189  isunitd  14201  invrfvald  14217  dvrfvald  14228  rdivmuldivd  14239  invrpropdg  14244  isrim0  14256  rhmunitinv  14273  subrgintm  14338  rrgmex  14356  aprval  14378  lssmex  14451  islss3  14475  sraval  14533  sralemg  14534  srascag  14538  sravscag  14539  sraipg  14540  sraex  14542  lidlmex  14571  lidlrsppropdg  14591  2idlmex  14597  qusrhm  14624  zrhval  14713  psrval  14762  psrbasg  14775  psrplusgg  14779  psraddcl  14781  psr0cl  14782  psr0lid  14783  psrnegcl  14784  psrlinv  14785  psrgrp  14786  psr1clfi  14789  mplsubgfilemcl  14800  istopon  14824  istps  14843  tgclb  14876  restbasg  14979  restco  14985  lmfval  15004  cnfval  15005  cnpfval  15006  cnpval  15009  txcnp  15082  txrest  15087  ismet2  15165  xmetpsmet  15180  mopnval  15253  comet  15310  reldvg  15490  dvmptclx  15529  lgseisenlem2  15890  1vgrex  15961  p1evtxdeqfilem  16252  p1evtxdeqfi  16253  p1evtxdp1fi  16254  upgriswlkdc  16301  eupth2lem3fi  16417  eupth2lembfi  16418  gfsumval  16809