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  4575  dmmptd  5454  tfr1onlemsucfn  6492  tfrcllemsucfn  6505  frecrdg  6560  unsnfidcel  7094  fnfi  7114  caseinl  7269  caseinr  7270  omniwomnimkv  7345  nninfdcinf  7349  acfun  7400  seq3val  10694  seqvalcd  10695  seqf1oglem2  10754  seqf1og  10755  hashennn  11014  wrdexg  11095  lswex  11136  swrdspsleq  11214  cats1un  11268  cats1fvd  11313  s3fv0g  11338  s3fv1g  11339  lcmval  12600  hashdvds  12758  ennnfonelemp1  12992  isstruct2r  13058  strnfvnd  13067  strfvssn  13069  strslfv2d  13090  setsslid  13098  basmex  13107  basmexd  13108  ressbas2d  13116  ressval3d  13120  prdsex  13317  prdsval  13321  prdsbaslemss  13322  imasival  13354  imasbas  13355  imasplusg  13356  imasmulr  13357  imasaddfn  13365  imasaddval  13366  imasaddf  13367  imasmulfn  13368  imasmulval  13369  imasmulf  13370  qusval  13371  qusaddflemg  13382  qusaddval  13383  qusaddf  13384  qusmulval  13385  qusmulf  13386  xpsfrnel  13392  xpsval  13400  ismgmn0  13406  igsumvalx  13437  gsumfzval  13439  gsumval2  13445  prdssgrpd  13463  ress0g  13491  prdsidlem  13495  prdsmndd  13496  prds0g  13497  ismhm  13509  mhmex  13510  0mhm  13534  prdsgrpd  13657  prdsinvgd  13658  qusgrp2  13665  mulgval  13674  mulgfng  13676  mulg1  13681  mulgnnp1  13682  mulgnndir  13703  issubg2m  13741  1nsgtrivd  13771  eqgval  13775  eqgen  13779  rngpropd  13933  qusrng  13936  issrg  13943  ringidss  14007  ringpropd  14016  qusring2  14044  dvdsrvald  14072  dvdsrd  14073  isunitd  14085  invrfvald  14101  dvrfvald  14112  rdivmuldivd  14123  invrpropdg  14128  isrim0  14140  rhmunitinv  14157  subrgintm  14222  rrgmex  14240  aprval  14261  lssmex  14334  islss3  14358  sraval  14416  sralemg  14417  srascag  14421  sravscag  14422  sraipg  14423  sraex  14425  lidlmex  14454  lidlrsppropdg  14474  2idlmex  14480  qusrhm  14507  zrhval  14596  psrval  14645  psrbasg  14653  psrplusgg  14657  psraddcl  14659  psr0cl  14660  psr0lid  14661  psrnegcl  14662  psrlinv  14663  psrgrp  14664  psr1clfi  14667  mplsubgfilemcl  14678  istopon  14702  istps  14721  tgclb  14754  restbasg  14857  restco  14863  lmfval  14882  cnfval  14883  cnpfval  14884  cnpval  14887  txcnp  14960  txrest  14965  ismet2  15043  xmetpsmet  15058  mopnval  15131  comet  15188  reldvg  15368  dvmptclx  15407  lgseisenlem2  15765  1vgrex  15836  upgriswlkdc  16101