Theorem elexd 2784

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

Syntax hints:   → wi 4   ∈ wcel 2175  Vcvv 2771

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-v 2773

This theorem is referenced by:  ifexd  4530  dmmptd  5405  tfr1onlemsucfn  6425  tfrcllemsucfn  6438  frecrdg  6493  unsnfidcel  7017  fnfi  7037  caseinl  7192  caseinr  7193  omniwomnimkv  7268  nninfdcinf  7272  acfun  7318  seq3val  10603  seqvalcd  10604  seqf1oglem2  10663  seqf1og  10664  hashennn  10923  wrdexg  11003  lcmval  12327  hashdvds  12485  ennnfonelemp1  12719  isstruct2r  12785  strnfvnd  12794  strfvssn  12796  strslfv2d  12817  setsslid  12825  basmex  12833  basmexd  12834  ressbas2d  12842  ressval3d  12846  prdsex  13043  prdsval  13047  prdsbaslemss  13048  imasival  13080  imasbas  13081  imasplusg  13082  imasmulr  13083  imasaddfn  13091  imasaddval  13092  imasaddf  13093  imasmulfn  13094  imasmulval  13095  imasmulf  13096  qusval  13097  qusaddflemg  13108  qusaddval  13109  qusaddf  13110  qusmulval  13111  qusmulf  13112  xpsfrnel  13118  xpsval  13126  ismgmn0  13132  igsumvalx  13163  gsumfzval  13165  gsumval2  13171  prdssgrpd  13189  ress0g  13217  prdsidlem  13221  prdsmndd  13222  prds0g  13223  ismhm  13235  mhmex  13236  0mhm  13260  prdsgrpd  13383  prdsinvgd  13384  qusgrp2  13391  mulgval  13400  mulgfng  13402  mulg1  13407  mulgnnp1  13408  mulgnndir  13429  issubg2m  13467  1nsgtrivd  13497  eqgval  13501  eqgen  13505  rngpropd  13659  qusrng  13662  issrg  13669  ringidss  13733  ringpropd  13742  qusring2  13770  dvdsrvald  13797  dvdsrd  13798  isunitd  13810  invrfvald  13826  dvrfvald  13837  rdivmuldivd  13848  invrpropdg  13853  isrim0  13865  rhmunitinv  13882  subrgintm  13947  rrgmex  13965  aprval  13986  lssmex  14059  islss3  14083  sraval  14141  sralemg  14142  srascag  14146  sravscag  14147  sraipg  14148  sraex  14150  lidlmex  14179  lidlrsppropdg  14199  2idlmex  14205  qusrhm  14232  zrhval  14321  psrval  14370  psrbasg  14378  psrplusgg  14382  psraddcl  14384  psr0cl  14385  psr0lid  14386  psrnegcl  14387  psrlinv  14388  psrgrp  14389  psr1clfi  14392  mplsubgfilemcl  14403  istopon  14427  istps  14446  tgclb  14479  restbasg  14582  restco  14588  lmfval  14606  cnfval  14608  cnpfval  14609  cnpval  14612  txcnp  14685  txrest  14690  ismet2  14768  xmetpsmet  14783  mopnval  14856  comet  14913  reldvg  15093  dvmptclx  15132  lgseisenlem2  15490  1vgrex  15559