Theorem elexd 2784

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

Syntax hints:   → wi 4   ∈ wcel 2175  Vcvv 2771

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-v 2773

This theorem is referenced by:  ifexd  4529  dmmptd  5400  tfr1onlemsucfn  6416  tfrcllemsucfn  6429  frecrdg  6484  unsnfidcel  7000  fnfi  7020  caseinl  7175  caseinr  7176  omniwomnimkv  7251  nninfdcinf  7255  acfun  7301  seq3val  10586  seqvalcd  10587  seqf1oglem2  10646  seqf1og  10647  hashennn  10906  wrdexg  10980  lcmval  12304  hashdvds  12462  ennnfonelemp1  12696  isstruct2r  12762  strnfvnd  12771  strfvssn  12773  strslfv2d  12794  setsslid  12802  basmex  12810  basmexd  12811  ressbas2d  12819  ressval3d  12823  prdsex  13019  prdsval  13023  prdsbaslemss  13024  imasival  13056  imasbas  13057  imasplusg  13058  imasmulr  13059  imasaddfn  13067  imasaddval  13068  imasaddf  13069  imasmulfn  13070  imasmulval  13071  imasmulf  13072  qusval  13073  qusaddflemg  13084  qusaddval  13085  qusaddf  13086  qusmulval  13087  qusmulf  13088  xpsfrnel  13094  xpsval  13102  ismgmn0  13108  igsumvalx  13139  gsumfzval  13141  gsumval2  13147  prdssgrpd  13165  ress0g  13193  prdsidlem  13197  prdsmndd  13198  prds0g  13199  ismhm  13211  mhmex  13212  0mhm  13236  prdsgrpd  13359  prdsinvgd  13360  qusgrp2  13367  mulgval  13376  mulgfng  13378  mulg1  13383  mulgnnp1  13384  mulgnndir  13405  issubg2m  13443  1nsgtrivd  13473  eqgval  13477  eqgen  13481  rngpropd  13635  qusrng  13638  issrg  13645  ringidss  13709  ringpropd  13718  qusring2  13746  dvdsrvald  13773  dvdsrd  13774  isunitd  13786  invrfvald  13802  dvrfvald  13813  rdivmuldivd  13824  invrpropdg  13829  isrim0  13841  rhmunitinv  13858  subrgintm  13923  rrgmex  13941  aprval  13962  lssmex  14035  islss3  14059  sraval  14117  sralemg  14118  srascag  14122  sravscag  14123  sraipg  14124  sraex  14126  lidlmex  14155  lidlrsppropdg  14175  2idlmex  14181  qusrhm  14208  zrhval  14297  psrval  14346  psrbasg  14354  psrplusgg  14358  psraddcl  14360  psr0cl  14361  psr0lid  14362  psrnegcl  14363  psrlinv  14364  psrgrp  14365  psr1clfi  14368  mplsubgfilemcl  14379  istopon  14403  istps  14422  tgclb  14455  restbasg  14558  restco  14564  lmfval  14582  cnfval  14584  cnpfval  14585  cnpval  14588  txcnp  14661  txrest  14666  ismet2  14744  xmetpsmet  14759  mopnval  14832  comet  14889  reldvg  15069  dvmptclx  15108  lgseisenlem2  15466