Theorem elexd 2743

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

Syntax hints:   → wi 4   ∈ wcel 2141  Vcvv 2730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-v 2732

This theorem is referenced by:  ifexd  4469  dmmptd  5328  tfr1onlemsucfn  6319  tfrcllemsucfn  6332  frecrdg  6387  unsnfidcel  6898  fnfi  6914  caseinl  7068  caseinr  7069  omniwomnimkv  7143  nninfdcinf  7147  acfun  7184  seq3val  10414  seqvalcd  10415  hashennn  10714  lcmval  12017  hashdvds  12175  ennnfonelemp1  12361  isstruct2r  12427  strnfvnd  12436  strfvssn  12438  strslfv2d  12458  setsslid  12466  basmex  12474  basmexd  12475  ressid2  12477  ressval2  12478  ismgmn0  12612  ismhm  12685  0mhm  12704  istopon  12805  istps  12824  tgclb  12859  restbasg  12962  restco  12968  lmfval  12986  cnfval  12988  cnpfval  12989  cnpval  12992  txcnp  13065  txrest  13070  ismet2  13148  xmetpsmet  13163  mopnval  13236  comet  13293  reldvg  13442  dvmptclx  13474