Theorem elexd 2725

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

Syntax hints:   → wi 4   ∈ wcel 2128  Vcvv 2712

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-v 2714

This theorem is referenced by:  ifexd  4442  dmmptd  5297  tfr1onlemsucfn  6281  tfrcllemsucfn  6294  frecrdg  6349  unsnfidcel  6858  fnfi  6874  caseinl  7025  caseinr  7026  omniwomnimkv  7093  acfun  7125  seq3val  10339  seqvalcd  10340  hashennn  10636  lcmval  11920  hashdvds  12073  ennnfonelemp1  12107  isstruct2r  12161  strnfvnd  12170  strfvssn  12172  strslfv2d  12192  setsslid  12200  ressid2  12209  ressval2  12210  istopon  12371  istps  12390  tgclb  12425  restbasg  12528  restco  12534  lmfval  12552  cnfval  12554  cnpfval  12555  cnpval  12558  txcnp  12631  txrest  12636  ismet2  12714  xmetpsmet  12729  mopnval  12802  comet  12859  reldvg  13008  dvmptclx  13040