Theorem elexd 2816

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

Syntax hints:   → wi 4   ∈ wcel 2202  Vcvv 2802

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  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 2804

This theorem is referenced by:  ifexd  4581  dmmptd  5463  tfr1onlemsucfn  6506  tfrcllemsucfn  6519  frecrdg  6574  unsnfidcel  7113  fnfi  7135  caseinl  7290  caseinr  7291  omniwomnimkv  7366  nninfdcinf  7370  acfun  7422  seq3val  10723  seqvalcd  10724  seqf1oglem2  10783  seqf1og  10784  hashennn  11043  wrdexg  11128  lswex  11169  ccatw2s1leng  11219  ccat2s1fvwd  11228  swrdspsleq  11252  cats1un  11306  cats1fvd  11351  s3fv0g  11376  s3fv1g  11377  s3fv2g  11378  lcmval  12640  hashdvds  12798  ennnfonelemp1  13032  isstruct2r  13098  strnfvnd  13107  strfvssn  13109  strslfv2d  13130  setsslid  13138  basmex  13147  basmexd  13148  ressbas2d  13156  ressval3d  13160  prdsex  13357  prdsval  13361  prdsbaslemss  13362  imasival  13394  imasbas  13395  imasplusg  13396  imasmulr  13397  imasaddfn  13405  imasaddval  13406  imasaddf  13407  imasmulfn  13408  imasmulval  13409  imasmulf  13410  qusval  13411  qusaddflemg  13422  qusaddval  13423  qusaddf  13424  qusmulval  13425  qusmulf  13426  xpsfrnel  13432  xpsval  13440  ismgmn0  13446  igsumvalx  13477  gsumfzval  13479  gsumval2  13485  prdssgrpd  13503  ress0g  13531  prdsidlem  13535  prdsmndd  13536  prds0g  13537  ismhm  13549  mhmex  13550  0mhm  13574  prdsgrpd  13697  prdsinvgd  13698  qusgrp2  13705  mulgval  13714  mulgfng  13716  mulg1  13721  mulgnnp1  13722  mulgnndir  13743  issubg2m  13781  1nsgtrivd  13811  eqgval  13815  eqgen  13819  rngpropd  13974  qusrng  13977  issrg  13984  ringidss  14048  ringpropd  14057  qusring2  14085  dvdsrvald  14113  dvdsrd  14114  isunitd  14126  invrfvald  14142  dvrfvald  14153  rdivmuldivd  14164  invrpropdg  14169  isrim0  14181  rhmunitinv  14198  subrgintm  14263  rrgmex  14281  aprval  14302  lssmex  14375  islss3  14399  sraval  14457  sralemg  14458  srascag  14462  sravscag  14463  sraipg  14464  sraex  14466  lidlmex  14495  lidlrsppropdg  14515  2idlmex  14521  qusrhm  14548  zrhval  14637  psrval  14686  psrbasg  14694  psrplusgg  14698  psraddcl  14700  psr0cl  14701  psr0lid  14702  psrnegcl  14703  psrlinv  14704  psrgrp  14705  psr1clfi  14708  mplsubgfilemcl  14719  istopon  14743  istps  14762  tgclb  14795  restbasg  14898  restco  14904  lmfval  14923  cnfval  14924  cnpfval  14925  cnpval  14928  txcnp  15001  txrest  15006  ismet2  15084  xmetpsmet  15099  mopnval  15172  comet  15229  reldvg  15409  dvmptclx  15448  lgseisenlem2  15806  1vgrex  15877  p1evtxdeqfilem  16168  p1evtxdeqfi  16169  p1evtxdp1fi  16170  upgriswlkdc  16217  eupth2lem3fi  16333  eupth2lembfi  16334  gfsumval  16707