Theorem elexd 2787

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

Syntax hints:   → wi 4   ∈ wcel 2177  Vcvv 2773

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-v 2775

This theorem is referenced by:  ifexd  4539  dmmptd  5416  tfr1onlemsucfn  6439  tfrcllemsucfn  6452  frecrdg  6507  unsnfidcel  7033  fnfi  7053  caseinl  7208  caseinr  7209  omniwomnimkv  7284  nninfdcinf  7288  acfun  7335  seq3val  10627  seqvalcd  10628  seqf1oglem2  10687  seqf1og  10688  hashennn  10947  wrdexg  11027  lswex  11067  swrdspsleq  11143  cats1un  11197  lcmval  12460  hashdvds  12618  ennnfonelemp1  12852  isstruct2r  12918  strnfvnd  12927  strfvssn  12929  strslfv2d  12950  setsslid  12958  basmex  12966  basmexd  12967  ressbas2d  12975  ressval3d  12979  prdsex  13176  prdsval  13180  prdsbaslemss  13181  imasival  13213  imasbas  13214  imasplusg  13215  imasmulr  13216  imasaddfn  13224  imasaddval  13225  imasaddf  13226  imasmulfn  13227  imasmulval  13228  imasmulf  13229  qusval  13230  qusaddflemg  13241  qusaddval  13242  qusaddf  13243  qusmulval  13244  qusmulf  13245  xpsfrnel  13251  xpsval  13259  ismgmn0  13265  igsumvalx  13296  gsumfzval  13298  gsumval2  13304  prdssgrpd  13322  ress0g  13350  prdsidlem  13354  prdsmndd  13355  prds0g  13356  ismhm  13368  mhmex  13369  0mhm  13393  prdsgrpd  13516  prdsinvgd  13517  qusgrp2  13524  mulgval  13533  mulgfng  13535  mulg1  13540  mulgnnp1  13541  mulgnndir  13562  issubg2m  13600  1nsgtrivd  13630  eqgval  13634  eqgen  13638  rngpropd  13792  qusrng  13795  issrg  13802  ringidss  13866  ringpropd  13875  qusring2  13903  dvdsrvald  13930  dvdsrd  13931  isunitd  13943  invrfvald  13959  dvrfvald  13970  rdivmuldivd  13981  invrpropdg  13986  isrim0  13998  rhmunitinv  14015  subrgintm  14080  rrgmex  14098  aprval  14119  lssmex  14192  islss3  14216  sraval  14274  sralemg  14275  srascag  14279  sravscag  14280  sraipg  14281  sraex  14283  lidlmex  14312  lidlrsppropdg  14332  2idlmex  14338  qusrhm  14365  zrhval  14454  psrval  14503  psrbasg  14511  psrplusgg  14515  psraddcl  14517  psr0cl  14518  psr0lid  14519  psrnegcl  14520  psrlinv  14521  psrgrp  14522  psr1clfi  14525  mplsubgfilemcl  14536  istopon  14560  istps  14579  tgclb  14612  restbasg  14715  restco  14721  lmfval  14739  cnfval  14741  cnpfval  14742  cnpval  14745  txcnp  14818  txrest  14823  ismet2  14901  xmetpsmet  14916  mopnval  14989  comet  15046  reldvg  15226  dvmptclx  15265  lgseisenlem2  15623  1vgrex  15694