Theorem elexd 2813

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 2811	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2200  Vcvv 2799

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2801

This theorem is referenced by:  ifexd  4574  dmmptd  5453  tfr1onlemsucfn  6484  tfrcllemsucfn  6497  frecrdg  6552  unsnfidcel  7079  fnfi  7099  caseinl  7254  caseinr  7255  omniwomnimkv  7330  nninfdcinf  7334  acfun  7385  seq3val  10677  seqvalcd  10678  seqf1oglem2  10737  seqf1og  10738  hashennn  10997  wrdexg  11077  lswex  11118  swrdspsleq  11194  cats1un  11248  cats1fvd  11293  s3fv0g  11318  s3fv1g  11319  lcmval  12580  hashdvds  12738  ennnfonelemp1  12972  isstruct2r  13038  strnfvnd  13047  strfvssn  13049  strslfv2d  13070  setsslid  13078  basmex  13087  basmexd  13088  ressbas2d  13096  ressval3d  13100  prdsex  13297  prdsval  13301  prdsbaslemss  13302  imasival  13334  imasbas  13335  imasplusg  13336  imasmulr  13337  imasaddfn  13345  imasaddval  13346  imasaddf  13347  imasmulfn  13348  imasmulval  13349  imasmulf  13350  qusval  13351  qusaddflemg  13362  qusaddval  13363  qusaddf  13364  qusmulval  13365  qusmulf  13366  xpsfrnel  13372  xpsval  13380  ismgmn0  13386  igsumvalx  13417  gsumfzval  13419  gsumval2  13425  prdssgrpd  13443  ress0g  13471  prdsidlem  13475  prdsmndd  13476  prds0g  13477  ismhm  13489  mhmex  13490  0mhm  13514  prdsgrpd  13637  prdsinvgd  13638  qusgrp2  13645  mulgval  13654  mulgfng  13656  mulg1  13661  mulgnnp1  13662  mulgnndir  13683  issubg2m  13721  1nsgtrivd  13751  eqgval  13755  eqgen  13759  rngpropd  13913  qusrng  13916  issrg  13923  ringidss  13987  ringpropd  13996  qusring2  14024  dvdsrvald  14051  dvdsrd  14052  isunitd  14064  invrfvald  14080  dvrfvald  14091  rdivmuldivd  14102  invrpropdg  14107  isrim0  14119  rhmunitinv  14136  subrgintm  14201  rrgmex  14219  aprval  14240  lssmex  14313  islss3  14337  sraval  14395  sralemg  14396  srascag  14400  sravscag  14401  sraipg  14402  sraex  14404  lidlmex  14433  lidlrsppropdg  14453  2idlmex  14459  qusrhm  14486  zrhval  14575  psrval  14624  psrbasg  14632  psrplusgg  14636  psraddcl  14638  psr0cl  14639  psr0lid  14640  psrnegcl  14641  psrlinv  14642  psrgrp  14643  psr1clfi  14646  mplsubgfilemcl  14657  istopon  14681  istps  14700  tgclb  14733  restbasg  14836  restco  14842  lmfval  14860  cnfval  14862  cnpfval  14863  cnpval  14866  txcnp  14939  txrest  14944  ismet2  15022  xmetpsmet  15037  mopnval  15110  comet  15167  reldvg  15347  dvmptclx  15386  lgseisenlem2  15744  1vgrex  15815