Theorem elexd 2790

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

Syntax hints:   -> wi 4   e. wcel 2178   _Vcvv 2776

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-v 2778

This theorem is referenced by:  ifexd  4549  dmmptd  5426  tfr1onlemsucfn  6449  tfrcllemsucfn  6462  frecrdg  6517  unsnfidcel  7044  fnfi  7064  caseinl  7219  caseinr  7220  omniwomnimkv  7295  nninfdcinf  7299  acfun  7350  seq3val  10642  seqvalcd  10643  seqf1oglem2  10702  seqf1og  10703  hashennn  10962  wrdexg  11042  lswex  11082  swrdspsleq  11158  cats1un  11212  lcmval  12500  hashdvds  12658  ennnfonelemp1  12892  isstruct2r  12958  strnfvnd  12967  strfvssn  12969  strslfv2d  12990  setsslid  12998  basmex  13006  basmexd  13007  ressbas2d  13015  ressval3d  13019  prdsex  13216  prdsval  13220  prdsbaslemss  13221  imasival  13253  imasbas  13254  imasplusg  13255  imasmulr  13256  imasaddfn  13264  imasaddval  13265  imasaddf  13266  imasmulfn  13267  imasmulval  13268  imasmulf  13269  qusval  13270  qusaddflemg  13281  qusaddval  13282  qusaddf  13283  qusmulval  13284  qusmulf  13285  xpsfrnel  13291  xpsval  13299  ismgmn0  13305  igsumvalx  13336  gsumfzval  13338  gsumval2  13344  prdssgrpd  13362  ress0g  13390  prdsidlem  13394  prdsmndd  13395  prds0g  13396  ismhm  13408  mhmex  13409  0mhm  13433  prdsgrpd  13556  prdsinvgd  13557  qusgrp2  13564  mulgval  13573  mulgfng  13575  mulg1  13580  mulgnnp1  13581  mulgnndir  13602  issubg2m  13640  1nsgtrivd  13670  eqgval  13674  eqgen  13678  rngpropd  13832  qusrng  13835  issrg  13842  ringidss  13906  ringpropd  13915  qusring2  13943  dvdsrvald  13970  dvdsrd  13971  isunitd  13983  invrfvald  13999  dvrfvald  14010  rdivmuldivd  14021  invrpropdg  14026  isrim0  14038  rhmunitinv  14055  subrgintm  14120  rrgmex  14138  aprval  14159  lssmex  14232  islss3  14256  sraval  14314  sralemg  14315  srascag  14319  sravscag  14320  sraipg  14321  sraex  14323  lidlmex  14352  lidlrsppropdg  14372  2idlmex  14378  qusrhm  14405  zrhval  14494  psrval  14543  psrbasg  14551  psrplusgg  14555  psraddcl  14557  psr0cl  14558  psr0lid  14559  psrnegcl  14560  psrlinv  14561  psrgrp  14562  psr1clfi  14565  mplsubgfilemcl  14576  istopon  14600  istps  14619  tgclb  14652  restbasg  14755  restco  14761  lmfval  14779  cnfval  14781  cnpfval  14782  cnpval  14785  txcnp  14858  txrest  14863  ismet2  14941  xmetpsmet  14956  mopnval  15029  comet  15086  reldvg  15266  dvmptclx  15305  lgseisenlem2  15663  1vgrex  15734