Theorem elexd 2835

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

Syntax hints:   → wi 4   ∈ wcel 2209  Vcvv 2821

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is referenced by:  ifexd  4625  dmmptd  5509  mptsuppd  6486  suppssfvg  6493  tfr1onlemsucfn  6601  tfrcllemsucfn  6614  frecrdg  6669  mapsnend  7089  mapunen  7141  unsnfidcel  7218  fnfi  7240  caseinl  7421  caseinr  7422  omniwomnimkv  7497  nninfdcinf  7501  acfun  7553  seq3val  10875  seqvalcd  10876  seqf1oglem2  10935  seqf1og  10936  hashennn  11197  wrdexg  11293  lswex  11334  ccatw2s1leng  11384  ccat2s1fvwd  11393  swrdspsleq  11417  cats1un  11471  cats1fvd  11516  s3fv0g  11541  s3fv1g  11542  s3fv2g  11543  s1s3d  11545  s1s4d  11546  s1s5d  11547  s1s6d  11548  s1s7d  11549  s2s2d  11550  s4s2d  11551  s4s3d  11552  s3s4d  11553  s2s5d  11554  s5s2d  11555  s4s4d  11556  lcmval  12819  ballotfilemsv  13231  ennnfonelemp1  13275  isstruct2r  13341  strnfvnd  13350  strfvssn  13352  strslfv2d  13373  setsslid  13381  basmex  13390  basmexd  13391  ressbas2d  13399  ressval3d  13403  imasival  13604  imasbas  13605  imasplusg  13606  imasmulr  13607  imasaddfn  13615  imasaddval  13616  imasaddf  13617  imasmulfn  13618  imasmulval  13619  imasmulf  13620  qusval  13621  qusaddflemg  13632  qusaddval  13633  qusaddf  13634  qusmulval  13635  qusmulf  13636  xpsfrnel  13642  ismgmn0  13655  gzsumvalx  13686  gzsumfzval  13688  gzsumval2  13691  ress0g  13733  ismhm  13745  mhmex  13746  0mhm  13770  qusgrp2  13893  mulgval  13902  mulgfng  13904  mulg1  13909  mulgnnp1  13910  mulgnndir  13931  issubg2m  13969  1nsgtrivd  13999  eqgval  14003  eqgen  14007  gsumvalfi  14129  prdsex  14149  prdsval  14150  prdsbaslemss  14151  prdssgrpd  14168  prdsidlem  14170  prdsmndd  14171  prds0g  14172  prdsgrpd  14174  prdsinvgd  14175  xpsval  14178  rngpropd  14229  qusrng  14232  issrg  14243  ringidss  14307  ringpropd  14316  qusring2  14344  opprringb  14359  dvdsrvald  14373  dvdsrd  14374  isunitd  14386  invrfvald  14402  dvrfvald  14413  rdivmuldivd  14424  invrpropdg  14429  isrim0  14441  rhmunitinv  14458  subrgintm  14524  rrgmex  14542  aprval  14564  aprprop  14574  lssmex  14664  islss3  14688  sraval  14746  sralemg  14747  srascag  14751  sravscag  14752  sraipg  14753  sraex  14755  lidlmex  14784  lidlrsppropdg  14804  2idlmex  14810  qusrhm  14837  zrhval  14924  psrval  14973  psrbasg  14988  psrplusgg  14992  psraddcl  14994  psr0cl  14995  psr0lid  14996  psrnegcl  14997  psrlinv  14998  psrgrp  14999  psr1clfi  15002  mplsubgfilemcl  15013  istopon  15037  istps  15056  tgclb  15089  restbasg  15192  restco  15198  lmfval  15217  cnfval  15218  cnpfval  15219  cnpval  15222  txcnp  15295  txrest  15300  ismet2  15378  xmetpsmet  15393  mopnval  15466  comet  15523  reldvg  15703  dvmptclx  15742  lgseisenlem2  16104  1vgrex  16175  p1evtxdeqfilem  16466  p1evtxdeqfi  16467  p1evtxdp1fi  16468  upgriswlkdc  16515  eupth2lem3fi  16631  eupth2lembfi  16632