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  4532  dmmptd  5408  tfr1onlemsucfn  6428  tfrcllemsucfn  6441  frecrdg  6496  unsnfidcel  7020  fnfi  7040  caseinl  7195  caseinr  7196  omniwomnimkv  7271  nninfdcinf  7275  acfun  7321  seq3val  10607  seqvalcd  10608  seqf1oglem2  10667  seqf1og  10668  hashennn  10927  wrdexg  11007  lswex  11047  swrdspsleq  11123  lcmval  12418  hashdvds  12576  ennnfonelemp1  12810  isstruct2r  12876  strnfvnd  12885  strfvssn  12887  strslfv2d  12908  setsslid  12916  basmex  12924  basmexd  12925  ressbas2d  12933  ressval3d  12937  prdsex  13134  prdsval  13138  prdsbaslemss  13139  imasival  13171  imasbas  13172  imasplusg  13173  imasmulr  13174  imasaddfn  13182  imasaddval  13183  imasaddf  13184  imasmulfn  13185  imasmulval  13186  imasmulf  13187  qusval  13188  qusaddflemg  13199  qusaddval  13200  qusaddf  13201  qusmulval  13202  qusmulf  13203  xpsfrnel  13209  xpsval  13217  ismgmn0  13223  igsumvalx  13254  gsumfzval  13256  gsumval2  13262  prdssgrpd  13280  ress0g  13308  prdsidlem  13312  prdsmndd  13313  prds0g  13314  ismhm  13326  mhmex  13327  0mhm  13351  prdsgrpd  13474  prdsinvgd  13475  qusgrp2  13482  mulgval  13491  mulgfng  13493  mulg1  13498  mulgnnp1  13499  mulgnndir  13520  issubg2m  13558  1nsgtrivd  13588  eqgval  13592  eqgen  13596  rngpropd  13750  qusrng  13753  issrg  13760  ringidss  13824  ringpropd  13833  qusring2  13861  dvdsrvald  13888  dvdsrd  13889  isunitd  13901  invrfvald  13917  dvrfvald  13928  rdivmuldivd  13939  invrpropdg  13944  isrim0  13956  rhmunitinv  13973  subrgintm  14038  rrgmex  14056  aprval  14077  lssmex  14150  islss3  14174  sraval  14232  sralemg  14233  srascag  14237  sravscag  14238  sraipg  14239  sraex  14241  lidlmex  14270  lidlrsppropdg  14290  2idlmex  14296  qusrhm  14323  zrhval  14412  psrval  14461  psrbasg  14469  psrplusgg  14473  psraddcl  14475  psr0cl  14476  psr0lid  14477  psrnegcl  14478  psrlinv  14479  psrgrp  14480  psr1clfi  14483  mplsubgfilemcl  14494  istopon  14518  istps  14537  tgclb  14570  restbasg  14673  restco  14679  lmfval  14697  cnfval  14699  cnpfval  14700  cnpval  14703  txcnp  14776  txrest  14781  ismet2  14859  xmetpsmet  14874  mopnval  14947  comet  15004  reldvg  15184  dvmptclx  15223  lgseisenlem2  15581  1vgrex  15650