Theorem elexd 2817

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

Syntax hints:   → wi 4   ∈ wcel 2202  Vcvv 2803

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  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 2805

This theorem is referenced by:  ifexd  4587  dmmptd  5470  mptsuppd  6434  suppssfvg  6441  tfr1onlemsucfn  6549  tfrcllemsucfn  6562  frecrdg  6617  unsnfidcel  7156  fnfi  7178  caseinl  7333  caseinr  7334  omniwomnimkv  7409  nninfdcinf  7413  acfun  7465  seq3val  10768  seqvalcd  10769  seqf1oglem2  10828  seqf1og  10829  hashennn  11088  wrdexg  11173  lswex  11214  ccatw2s1leng  11264  ccat2s1fvwd  11273  swrdspsleq  11297  cats1un  11351  cats1fvd  11396  s3fv0g  11421  s3fv1g  11422  s3fv2g  11423  s1s3d  11425  s1s4d  11426  s1s5d  11427  s1s6d  11428  s1s7d  11429  s2s2d  11430  s4s2d  11431  s4s3d  11432  s3s4d  11433  s2s5d  11434  s5s2d  11435  s4s4d  11436  lcmval  12698  hashdvds  12856  ennnfonelemp1  13090  isstruct2r  13156  strnfvnd  13165  strfvssn  13167  strslfv2d  13188  setsslid  13196  basmex  13205  basmexd  13206  ressbas2d  13214  ressval3d  13218  prdsex  13415  prdsval  13419  prdsbaslemss  13420  imasival  13452  imasbas  13453  imasplusg  13454  imasmulr  13455  imasaddfn  13463  imasaddval  13464  imasaddf  13465  imasmulfn  13466  imasmulval  13467  imasmulf  13468  qusval  13469  qusaddflemg  13480  qusaddval  13481  qusaddf  13482  qusmulval  13483  qusmulf  13484  xpsfrnel  13490  xpsval  13498  ismgmn0  13504  igsumvalx  13535  gsumfzval  13537  gsumval2  13543  prdssgrpd  13561  ress0g  13589  prdsidlem  13593  prdsmndd  13594  prds0g  13595  ismhm  13607  mhmex  13608  0mhm  13632  prdsgrpd  13755  prdsinvgd  13756  qusgrp2  13763  mulgval  13772  mulgfng  13774  mulg1  13779  mulgnnp1  13780  mulgnndir  13801  issubg2m  13839  1nsgtrivd  13869  eqgval  13873  eqgen  13877  rngpropd  14032  qusrng  14035  issrg  14042  ringidss  14106  ringpropd  14115  qusring2  14143  dvdsrvald  14171  dvdsrd  14172  isunitd  14184  invrfvald  14200  dvrfvald  14211  rdivmuldivd  14222  invrpropdg  14227  isrim0  14239  rhmunitinv  14256  subrgintm  14321  rrgmex  14339  aprval  14361  lssmex  14434  islss3  14458  sraval  14516  sralemg  14517  srascag  14521  sravscag  14522  sraipg  14523  sraex  14525  lidlmex  14554  lidlrsppropdg  14574  2idlmex  14580  qusrhm  14607  zrhval  14696  psrval  14745  psrbasg  14758  psrplusgg  14762  psraddcl  14764  psr0cl  14765  psr0lid  14766  psrnegcl  14767  psrlinv  14768  psrgrp  14769  psr1clfi  14772  mplsubgfilemcl  14783  istopon  14807  istps  14826  tgclb  14859  restbasg  14962  restco  14968  lmfval  14987  cnfval  14988  cnpfval  14989  cnpval  14992  txcnp  15065  txrest  15070  ismet2  15148  xmetpsmet  15163  mopnval  15236  comet  15293  reldvg  15473  dvmptclx  15512  lgseisenlem2  15873  1vgrex  15944  p1evtxdeqfilem  16235  p1evtxdeqfi  16236  p1evtxdp1fi  16237  upgriswlkdc  16284  eupth2lem3fi  16400  eupth2lembfi  16401  gfsumval  16792