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  4576  dmmptd  5457  tfr1onlemsucfn  6497  tfrcllemsucfn  6510  frecrdg  6565  unsnfidcel  7099  fnfi  7119  caseinl  7274  caseinr  7275  omniwomnimkv  7350  nninfdcinf  7354  acfun  7405  seq3val  10699  seqvalcd  10700  seqf1oglem2  10759  seqf1og  10760  hashennn  11019  wrdexg  11100  lswex  11141  swrdspsleq  11220  cats1un  11274  cats1fvd  11319  s3fv0g  11344  s3fv1g  11345  lcmval  12606  hashdvds  12764  ennnfonelemp1  12998  isstruct2r  13064  strnfvnd  13073  strfvssn  13075  strslfv2d  13096  setsslid  13104  basmex  13113  basmexd  13114  ressbas2d  13122  ressval3d  13126  prdsex  13323  prdsval  13327  prdsbaslemss  13328  imasival  13360  imasbas  13361  imasplusg  13362  imasmulr  13363  imasaddfn  13371  imasaddval  13372  imasaddf  13373  imasmulfn  13374  imasmulval  13375  imasmulf  13376  qusval  13377  qusaddflemg  13388  qusaddval  13389  qusaddf  13390  qusmulval  13391  qusmulf  13392  xpsfrnel  13398  xpsval  13406  ismgmn0  13412  igsumvalx  13443  gsumfzval  13445  gsumval2  13451  prdssgrpd  13469  ress0g  13497  prdsidlem  13501  prdsmndd  13502  prds0g  13503  ismhm  13515  mhmex  13516  0mhm  13540  prdsgrpd  13663  prdsinvgd  13664  qusgrp2  13671  mulgval  13680  mulgfng  13682  mulg1  13687  mulgnnp1  13688  mulgnndir  13709  issubg2m  13747  1nsgtrivd  13777  eqgval  13781  eqgen  13785  rngpropd  13939  qusrng  13942  issrg  13949  ringidss  14013  ringpropd  14022  qusring2  14050  dvdsrvald  14078  dvdsrd  14079  isunitd  14091  invrfvald  14107  dvrfvald  14118  rdivmuldivd  14129  invrpropdg  14134  isrim0  14146  rhmunitinv  14163  subrgintm  14228  rrgmex  14246  aprval  14267  lssmex  14340  islss3  14364  sraval  14422  sralemg  14423  srascag  14427  sravscag  14428  sraipg  14429  sraex  14431  lidlmex  14460  lidlrsppropdg  14480  2idlmex  14486  qusrhm  14513  zrhval  14602  psrval  14651  psrbasg  14659  psrplusgg  14663  psraddcl  14665  psr0cl  14666  psr0lid  14667  psrnegcl  14668  psrlinv  14669  psrgrp  14670  psr1clfi  14673  mplsubgfilemcl  14684  istopon  14708  istps  14727  tgclb  14760  restbasg  14863  restco  14869  lmfval  14888  cnfval  14889  cnpfval  14890  cnpval  14893  txcnp  14966  txrest  14971  ismet2  15049  xmetpsmet  15064  mopnval  15137  comet  15194  reldvg  15374  dvmptclx  15413  lgseisenlem2  15771  1vgrex  15842  upgriswlkdc  16132