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  7290  seq3val  10569  seqvalcd  10570  seqf1oglem2  10629  seqf1og  10630  hashennn  10889  wrdexg  10963  lcmval  12256  hashdvds  12414  ennnfonelemp1  12648  isstruct2r  12714  strnfvnd  12723  strfvssn  12725  strslfv2d  12746  setsslid  12754  basmex  12762  basmexd  12763  ressbas2d  12771  ressval3d  12775  prdsex  12971  prdsval  12975  prdsbaslemss  12976  imasival  13008  imasbas  13009  imasplusg  13010  imasmulr  13011  imasaddfn  13019  imasaddval  13020  imasaddf  13021  imasmulfn  13022  imasmulval  13023  imasmulf  13024  qusval  13025  qusaddflemg  13036  qusaddval  13037  qusaddf  13038  qusmulval  13039  qusmulf  13040  xpsfrnel  13046  xpsval  13054  ismgmn0  13060  igsumvalx  13091  gsumfzval  13093  gsumval2  13099  prdssgrpd  13117  ress0g  13145  prdsidlem  13149  prdsmndd  13150  prds0g  13151  ismhm  13163  mhmex  13164  0mhm  13188  prdsgrpd  13311  prdsinvgd  13312  qusgrp2  13319  mulgval  13328  mulgfng  13330  mulg1  13335  mulgnnp1  13336  mulgnndir  13357  issubg2m  13395  1nsgtrivd  13425  eqgval  13429  eqgen  13433  rngpropd  13587  qusrng  13590  issrg  13597  ringidss  13661  ringpropd  13670  qusring2  13698  dvdsrvald  13725  dvdsrd  13726  isunitd  13738  invrfvald  13754  dvrfvald  13765  rdivmuldivd  13776  invrpropdg  13781  isrim0  13793  rhmunitinv  13810  subrgintm  13875  rrgmex  13893  aprval  13914  lssmex  13987  islss3  14011  sraval  14069  sralemg  14070  srascag  14074  sravscag  14075  sraipg  14076  sraex  14078  lidlmex  14107  lidlrsppropdg  14127  2idlmex  14133  qusrhm  14160  zrhval  14249  psrval  14296  psrbasg  14303  psrplusgg  14306  psraddcl  14308  psr0cl  14309  psr0lid  14310  psrnegcl  14311  psrlinv  14312  psrgrp  14313  psr1clfi  14316  istopon  14333  istps  14352  tgclb  14385  restbasg  14488  restco  14494  lmfval  14512  cnfval  14514  cnpfval  14515  cnpval  14518  txcnp  14591  txrest  14596  ismet2  14674  xmetpsmet  14689  mopnval  14762  comet  14819  reldvg  14999  dvmptclx  15038  lgseisenlem2  15396