Theorem elexd 2776

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

Syntax hints:   → wi 4   ∈ wcel 2167  Vcvv 2763

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765

This theorem is referenced by:  ifexd  4520  dmmptd  5391  tfr1onlemsucfn  6407  tfrcllemsucfn  6420  frecrdg  6475  unsnfidcel  6991  fnfi  7011  caseinl  7166  caseinr  7167  omniwomnimkv  7242  nninfdcinf  7246  acfun  7292  seq3val  10571  seqvalcd  10572  seqf1oglem2  10631  seqf1og  10632  hashennn  10891  wrdexg  10965  lcmval  12258  hashdvds  12416  ennnfonelemp1  12650  isstruct2r  12716  strnfvnd  12725  strfvssn  12727  strslfv2d  12748  setsslid  12756  basmex  12764  basmexd  12765  ressbas2d  12773  ressval3d  12777  prdsex  12973  prdsval  12977  prdsbaslemss  12978  imasival  13010  imasbas  13011  imasplusg  13012  imasmulr  13013  imasaddfn  13021  imasaddval  13022  imasaddf  13023  imasmulfn  13024  imasmulval  13025  imasmulf  13026  qusval  13027  qusaddflemg  13038  qusaddval  13039  qusaddf  13040  qusmulval  13041  qusmulf  13042  xpsfrnel  13048  xpsval  13056  ismgmn0  13062  igsumvalx  13093  gsumfzval  13095  gsumval2  13101  prdssgrpd  13119  ress0g  13147  prdsidlem  13151  prdsmndd  13152  prds0g  13153  ismhm  13165  mhmex  13166  0mhm  13190  prdsgrpd  13313  prdsinvgd  13314  qusgrp2  13321  mulgval  13330  mulgfng  13332  mulg1  13337  mulgnnp1  13338  mulgnndir  13359  issubg2m  13397  1nsgtrivd  13427  eqgval  13431  eqgen  13435  rngpropd  13589  qusrng  13592  issrg  13599  ringidss  13663  ringpropd  13672  qusring2  13700  dvdsrvald  13727  dvdsrd  13728  isunitd  13740  invrfvald  13756  dvrfvald  13767  rdivmuldivd  13778  invrpropdg  13783  isrim0  13795  rhmunitinv  13812  subrgintm  13877  rrgmex  13895  aprval  13916  lssmex  13989  islss3  14013  sraval  14071  sralemg  14072  srascag  14076  sravscag  14077  sraipg  14078  sraex  14080  lidlmex  14109  lidlrsppropdg  14129  2idlmex  14135  qusrhm  14162  zrhval  14251  psrval  14300  psrbasg  14308  psrplusgg  14312  psraddcl  14314  psr0cl  14315  psr0lid  14316  psrnegcl  14317  psrlinv  14318  psrgrp  14319  psr1clfi  14322  mplsubgfilemcl  14333  istopon  14357  istps  14376  tgclb  14409  restbasg  14512  restco  14518  lmfval  14536  cnfval  14538  cnpfval  14539  cnpval  14542  txcnp  14615  txrest  14620  ismet2  14698  xmetpsmet  14713  mopnval  14786  comet  14843  reldvg  15023  dvmptclx  15062  lgseisenlem2  15420