Theorem elexd 2785

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

Syntax hints:   -> wi 4   e. wcel 2176   _Vcvv 2772

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-v 2774

This theorem is referenced by:  ifexd  4531  dmmptd  5406  tfr1onlemsucfn  6426  tfrcllemsucfn  6439  frecrdg  6494  unsnfidcel  7018  fnfi  7038  caseinl  7193  caseinr  7194  omniwomnimkv  7269  nninfdcinf  7273  acfun  7319  seq3val  10605  seqvalcd  10606  seqf1oglem2  10665  seqf1og  10666  hashennn  10925  wrdexg  11005  swrdspsleq  11120  lcmval  12385  hashdvds  12543  ennnfonelemp1  12777  isstruct2r  12843  strnfvnd  12852  strfvssn  12854  strslfv2d  12875  setsslid  12883  basmex  12891  basmexd  12892  ressbas2d  12900  ressval3d  12904  prdsex  13101  prdsval  13105  prdsbaslemss  13106  imasival  13138  imasbas  13139  imasplusg  13140  imasmulr  13141  imasaddfn  13149  imasaddval  13150  imasaddf  13151  imasmulfn  13152  imasmulval  13153  imasmulf  13154  qusval  13155  qusaddflemg  13166  qusaddval  13167  qusaddf  13168  qusmulval  13169  qusmulf  13170  xpsfrnel  13176  xpsval  13184  ismgmn0  13190  igsumvalx  13221  gsumfzval  13223  gsumval2  13229  prdssgrpd  13247  ress0g  13275  prdsidlem  13279  prdsmndd  13280  prds0g  13281  ismhm  13293  mhmex  13294  0mhm  13318  prdsgrpd  13441  prdsinvgd  13442  qusgrp2  13449  mulgval  13458  mulgfng  13460  mulg1  13465  mulgnnp1  13466  mulgnndir  13487  issubg2m  13525  1nsgtrivd  13555  eqgval  13559  eqgen  13563  rngpropd  13717  qusrng  13720  issrg  13727  ringidss  13791  ringpropd  13800  qusring2  13828  dvdsrvald  13855  dvdsrd  13856  isunitd  13868  invrfvald  13884  dvrfvald  13895  rdivmuldivd  13906  invrpropdg  13911  isrim0  13923  rhmunitinv  13940  subrgintm  14005  rrgmex  14023  aprval  14044  lssmex  14117  islss3  14141  sraval  14199  sralemg  14200  srascag  14204  sravscag  14205  sraipg  14206  sraex  14208  lidlmex  14237  lidlrsppropdg  14257  2idlmex  14263  qusrhm  14290  zrhval  14379  psrval  14428  psrbasg  14436  psrplusgg  14440  psraddcl  14442  psr0cl  14443  psr0lid  14444  psrnegcl  14445  psrlinv  14446  psrgrp  14447  psr1clfi  14450  mplsubgfilemcl  14461  istopon  14485  istps  14504  tgclb  14537  restbasg  14640  restco  14646  lmfval  14664  cnfval  14666  cnpfval  14667  cnpval  14670  txcnp  14743  txrest  14748  ismet2  14826  xmetpsmet  14841  mopnval  14914  comet  14971  reldvg  15151  dvmptclx  15190  lgseisenlem2  15548  1vgrex  15617