Theorem elexd 2829

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

Syntax hints:   → wi 4   ∈ wcel 2205  Vcvv 2815

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 2216

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-v 2817

This theorem is referenced by:  ifexd  4610  dmmptd  5494  mptsuppd  6469  suppssfvg  6476  tfr1onlemsucfn  6584  tfrcllemsucfn  6597  frecrdg  6652  mapsnend  7065  mapunen  7117  unsnfidcel  7194  fnfi  7216  caseinl  7395  caseinr  7396  omniwomnimkv  7471  nninfdcinf  7475  acfun  7527  seq3val  10846  seqvalcd  10847  seqf1oglem2  10906  seqf1og  10907  hashennn  11168  wrdexg  11260  lswex  11301  ccatw2s1leng  11351  ccat2s1fvwd  11360  swrdspsleq  11384  cats1un  11438  cats1fvd  11483  s3fv0g  11508  s3fv1g  11509  s3fv2g  11510  s1s3d  11512  s1s4d  11513  s1s5d  11514  s1s6d  11515  s1s7d  11516  s2s2d  11517  s4s2d  11518  s4s3d  11519  s3s4d  11520  s2s5d  11521  s5s2d  11522  s4s4d  11523  lcmval  12785  ballotfilemsv  13197  ennnfonelemp1  13241  isstruct2r  13307  strnfvnd  13316  strfvssn  13318  strslfv2d  13339  setsslid  13347  basmex  13356  basmexd  13357  ressbas2d  13365  ressval3d  13369  imasival  13570  imasbas  13571  imasplusg  13572  imasmulr  13573  imasaddfn  13581  imasaddval  13582  imasaddf  13583  imasmulfn  13584  imasmulval  13585  imasmulf  13586  qusval  13587  qusaddflemg  13598  qusaddval  13599  qusaddf  13600  qusmulval  13601  qusmulf  13602  xpsfrnel  13608  ismgmn0  13621  igsumvalx  13652  gsumfzval  13654  gsumval2  13660  ress0g  13704  ismhm  13716  mhmex  13717  0mhm  13741  qusgrp2  13866  mulgval  13875  mulgfng  13877  mulg1  13882  mulgnnp1  13883  mulgnndir  13904  issubg2m  13942  1nsgtrivd  13972  eqgval  13976  eqgen  13980  gfsumval  14102  prdsex  14114  prdsval  14115  prdsbaslemss  14116  prdssgrpd  14133  prdsidlem  14135  prdsmndd  14136  prds0g  14137  prdsgrpd  14139  prdsinvgd  14140  xpsval  14143  rngpropd  14194  qusrng  14197  issrg  14208  ringidss  14272  ringpropd  14281  qusring2  14309  opprringb  14324  dvdsrvald  14338  dvdsrd  14339  isunitd  14351  invrfvald  14367  dvrfvald  14378  rdivmuldivd  14389  invrpropdg  14394  isrim0  14406  rhmunitinv  14423  subrgintm  14489  rrgmex  14507  aprval  14529  aprprop  14539  lssmex  14629  islss3  14653  sraval  14711  sralemg  14712  srascag  14716  sravscag  14717  sraipg  14718  sraex  14720  lidlmex  14749  lidlrsppropdg  14769  2idlmex  14775  qusrhm  14802  zrhval  14891  psrval  14940  psrbasg  14955  psrplusgg  14959  psraddcl  14961  psr0cl  14962  psr0lid  14963  psrnegcl  14964  psrlinv  14965  psrgrp  14966  psr1clfi  14969  mplsubgfilemcl  14980  istopon  15004  istps  15023  tgclb  15056  restbasg  15159  restco  15165  lmfval  15184  cnfval  15185  cnpfval  15186  cnpval  15189  txcnp  15262  txrest  15267  ismet2  15345  xmetpsmet  15360  mopnval  15433  comet  15490  reldvg  15670  dvmptclx  15709  lgseisenlem2  16070  1vgrex  16141  p1evtxdeqfilem  16432  p1evtxdeqfi  16433  p1evtxdp1fi  16434  upgriswlkdc  16481  eupth2lem3fi  16597  eupth2lembfi  16598