Theorem elexd 2816

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	⊢ (𝜑 → 𝐴 ∈ 𝑉)

Assertion

Ref	Expression
elexd	⊢ (𝜑 → 𝐴 ∈ V)

Proof of Theorem elexd

Step	Hyp	Ref	Expression
1		elexd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		elex 2814	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2202  Vcvv 2802

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  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 2804

This theorem is referenced by:  ifexd  4581  dmmptd  5463  tfr1onlemsucfn  6505  tfrcllemsucfn  6518  frecrdg  6573  unsnfidcel  7112  fnfi  7134  caseinl  7289  caseinr  7290  omniwomnimkv  7365  nninfdcinf  7369  acfun  7421  seq3val  10721  seqvalcd  10722  seqf1oglem2  10781  seqf1og  10782  hashennn  11041  wrdexg  11123  lswex  11164  ccatw2s1leng  11214  ccat2s1fvwd  11223  swrdspsleq  11247  cats1un  11301  cats1fvd  11346  s3fv0g  11371  s3fv1g  11372  s3fv2g  11373  lcmval  12634  hashdvds  12792  ennnfonelemp1  13026  isstruct2r  13092  strnfvnd  13101  strfvssn  13103  strslfv2d  13124  setsslid  13132  basmex  13141  basmexd  13142  ressbas2d  13150  ressval3d  13154  prdsex  13351  prdsval  13355  prdsbaslemss  13356  imasival  13388  imasbas  13389  imasplusg  13390  imasmulr  13391  imasaddfn  13399  imasaddval  13400  imasaddf  13401  imasmulfn  13402  imasmulval  13403  imasmulf  13404  qusval  13405  qusaddflemg  13416  qusaddval  13417  qusaddf  13418  qusmulval  13419  qusmulf  13420  xpsfrnel  13426  xpsval  13434  ismgmn0  13440  igsumvalx  13471  gsumfzval  13473  gsumval2  13479  prdssgrpd  13497  ress0g  13525  prdsidlem  13529  prdsmndd  13530  prds0g  13531  ismhm  13543  mhmex  13544  0mhm  13568  prdsgrpd  13691  prdsinvgd  13692  qusgrp2  13699  mulgval  13708  mulgfng  13710  mulg1  13715  mulgnnp1  13716  mulgnndir  13737  issubg2m  13775  1nsgtrivd  13805  eqgval  13809  eqgen  13813  rngpropd  13967  qusrng  13970  issrg  13977  ringidss  14041  ringpropd  14050  qusring2  14078  dvdsrvald  14106  dvdsrd  14107  isunitd  14119  invrfvald  14135  dvrfvald  14146  rdivmuldivd  14157  invrpropdg  14162  isrim0  14174  rhmunitinv  14191  subrgintm  14256  rrgmex  14274  aprval  14295  lssmex  14368  islss3  14392  sraval  14450  sralemg  14451  srascag  14455  sravscag  14456  sraipg  14457  sraex  14459  lidlmex  14488  lidlrsppropdg  14508  2idlmex  14514  qusrhm  14541  zrhval  14630  psrval  14679  psrbasg  14687  psrplusgg  14691  psraddcl  14693  psr0cl  14694  psr0lid  14695  psrnegcl  14696  psrlinv  14697  psrgrp  14698  psr1clfi  14701  mplsubgfilemcl  14712  istopon  14736  istps  14755  tgclb  14788  restbasg  14891  restco  14897  lmfval  14916  cnfval  14917  cnpfval  14918  cnpval  14921  txcnp  14994  txrest  14999  ismet2  15077  xmetpsmet  15092  mopnval  15165  comet  15222  reldvg  15402  dvmptclx  15441  lgseisenlem2  15799  1vgrex  15870  p1evtxdeqfilem  16161  p1evtxdeqfi  16162  p1evtxdp1fi  16163  upgriswlkdc  16210  gfsumval  16680