Theorem elexd 2773

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

Syntax hints:   -> wi 4   e. wcel 2164   _Vcvv 2760

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-v 2762

This theorem is referenced by:  ifexd  4515  dmmptd  5384  tfr1onlemsucfn  6393  tfrcllemsucfn  6406  frecrdg  6461  unsnfidcel  6977  fnfi  6995  caseinl  7150  caseinr  7151  omniwomnimkv  7226  nninfdcinf  7230  acfun  7267  seq3val  10531  seqvalcd  10532  seqf1oglem2  10591  seqf1og  10592  hashennn  10851  wrdexg  10925  lcmval  12201  hashdvds  12359  ennnfonelemp1  12563  isstruct2r  12629  strnfvnd  12638  strfvssn  12640  strslfv2d  12661  setsslid  12669  basmex  12677  basmexd  12678  ressbas2d  12686  ressval3d  12690  prdsex  12880  imasival  12889  imasbas  12890  imasplusg  12891  imasmulr  12892  imasaddfn  12900  imasaddval  12901  imasaddf  12902  imasmulfn  12903  imasmulval  12904  imasmulf  12905  qusval  12906  qusaddflemg  12917  qusaddval  12918  qusaddf  12919  qusmulval  12920  qusmulf  12921  xpsfrnel  12927  xpsval  12935  ismgmn0  12941  igsumvalx  12972  gsumfzval  12974  gsumval2  12980  ress0g  13024  ismhm  13033  mhmex  13034  0mhm  13058  qusgrp2  13183  mulgval  13192  mulgfng  13194  mulg1  13199  mulgnnp1  13200  mulgnndir  13221  issubg2m  13259  1nsgtrivd  13289  eqgval  13293  eqgen  13297  rngpropd  13451  qusrng  13454  issrg  13461  ringidss  13525  ringpropd  13534  qusring2  13562  dvdsrvald  13589  dvdsrd  13590  isunitd  13602  invrfvald  13618  dvrfvald  13629  rdivmuldivd  13640  invrpropdg  13645  isrim0  13657  rhmunitinv  13674  subrgintm  13739  rrgmex  13757  aprval  13778  lssmex  13851  islss3  13875  sraval  13933  sralemg  13934  srascag  13938  sravscag  13939  sraipg  13940  sraex  13942  lidlmex  13971  lidlrsppropdg  13991  2idlmex  13997  qusrhm  14024  zrhval  14105  psrval  14152  psrbasg  14159  psrplusgg  14162  psraddcl  14164  istopon  14181  istps  14200  tgclb  14233  restbasg  14336  restco  14342  lmfval  14360  cnfval  14362  cnpfval  14363  cnpval  14366  txcnp  14439  txrest  14444  ismet2  14522  xmetpsmet  14537  mopnval  14610  comet  14667  reldvg  14833  dvmptclx  14865  lgseisenlem2  15187