Theorem elexd 2702

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

Syntax hints:   → wi 4   ∈ wcel 1481  Vcvv 2689

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-v 2691

This theorem is referenced by:  dmmptd  5261  tfr1onlemsucfn  6245  tfrcllemsucfn  6258  frecrdg  6313  unsnfidcel  6817  fnfi  6833  caseinl  6984  caseinr  6985  omniwomnimkv  7049  acfun  7080  seq3val  10262  seqvalcd  10263  hashennn  10558  lcmval  11780  hashdvds  11933  ennnfonelemp1  11955  isstruct2r  12009  strnfvnd  12018  strfvssn  12020  strslfv2d  12040  setsslid  12048  ressid2  12057  ressval2  12058  istopon  12219  istps  12238  tgclb  12273  restbasg  12376  restco  12382  lmfval  12400  cnfval  12402  cnpfval  12403  cnpval  12406  txcnp  12479  txrest  12484  ismet2  12562  xmetpsmet  12577  mopnval  12650  comet  12707  reldvg  12856  dvmptclx  12888