Theorem elexd 2814

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

Syntax hints:   → wi 4   ∈ wcel 2200  Vcvv 2800

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 2802

This theorem is referenced by:  ifexd  4579  dmmptd  5460  tfr1onlemsucfn  6501  tfrcllemsucfn  6514  frecrdg  6569  unsnfidcel  7106  fnfi  7126  caseinl  7281  caseinr  7282  omniwomnimkv  7357  nninfdcinf  7361  acfun  7412  seq3val  10712  seqvalcd  10713  seqf1oglem2  10772  seqf1og  10773  hashennn  11032  wrdexg  11114  lswex  11155  ccatw2s1leng  11205  ccat2s1fvwd  11214  swrdspsleq  11238  cats1un  11292  cats1fvd  11337  s3fv0g  11362  s3fv1g  11363  s3fv2g  11364  lcmval  12625  hashdvds  12783  ennnfonelemp1  13017  isstruct2r  13083  strnfvnd  13092  strfvssn  13094  strslfv2d  13115  setsslid  13123  basmex  13132  basmexd  13133  ressbas2d  13141  ressval3d  13145  prdsex  13342  prdsval  13346  prdsbaslemss  13347  imasival  13379  imasbas  13380  imasplusg  13381  imasmulr  13382  imasaddfn  13390  imasaddval  13391  imasaddf  13392  imasmulfn  13393  imasmulval  13394  imasmulf  13395  qusval  13396  qusaddflemg  13407  qusaddval  13408  qusaddf  13409  qusmulval  13410  qusmulf  13411  xpsfrnel  13417  xpsval  13425  ismgmn0  13431  igsumvalx  13462  gsumfzval  13464  gsumval2  13470  prdssgrpd  13488  ress0g  13516  prdsidlem  13520  prdsmndd  13521  prds0g  13522  ismhm  13534  mhmex  13535  0mhm  13559  prdsgrpd  13682  prdsinvgd  13683  qusgrp2  13690  mulgval  13699  mulgfng  13701  mulg1  13706  mulgnnp1  13707  mulgnndir  13728  issubg2m  13766  1nsgtrivd  13796  eqgval  13800  eqgen  13804  rngpropd  13958  qusrng  13961  issrg  13968  ringidss  14032  ringpropd  14041  qusring2  14069  dvdsrvald  14097  dvdsrd  14098  isunitd  14110  invrfvald  14126  dvrfvald  14137  rdivmuldivd  14148  invrpropdg  14153  isrim0  14165  rhmunitinv  14182  subrgintm  14247  rrgmex  14265  aprval  14286  lssmex  14359  islss3  14383  sraval  14441  sralemg  14442  srascag  14446  sravscag  14447  sraipg  14448  sraex  14450  lidlmex  14479  lidlrsppropdg  14499  2idlmex  14505  qusrhm  14532  zrhval  14621  psrval  14670  psrbasg  14678  psrplusgg  14682  psraddcl  14684  psr0cl  14685  psr0lid  14686  psrnegcl  14687  psrlinv  14688  psrgrp  14689  psr1clfi  14692  mplsubgfilemcl  14703  istopon  14727  istps  14746  tgclb  14779  restbasg  14882  restco  14888  lmfval  14907  cnfval  14908  cnpfval  14909  cnpval  14912  txcnp  14985  txrest  14990  ismet2  15068  xmetpsmet  15083  mopnval  15156  comet  15213  reldvg  15393  dvmptclx  15432  lgseisenlem2  15790  1vgrex  15861  upgriswlkdc  16157