Theorem elexd 2739

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

Syntax hints:   → wi 4   ∈ wcel 2136  Vcvv 2726

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-v 2728

This theorem is referenced by:  ifexd  4462  dmmptd  5318  tfr1onlemsucfn  6308  tfrcllemsucfn  6321  frecrdg  6376  unsnfidcel  6886  fnfi  6902  caseinl  7056  caseinr  7057  omniwomnimkv  7131  acfun  7163  seq3val  10393  seqvalcd  10394  hashennn  10693  lcmval  11995  hashdvds  12153  ennnfonelemp1  12339  isstruct2r  12405  strnfvnd  12414  strfvssn  12416  strslfv2d  12436  setsslid  12444  basmex  12452  ressid2  12454  ressval2  12455  ismgmn0  12589  istopon  12651  istps  12670  tgclb  12705  restbasg  12808  restco  12814  lmfval  12832  cnfval  12834  cnpfval  12835  cnpval  12838  txcnp  12911  txrest  12916  ismet2  12994  xmetpsmet  13009  mopnval  13082  comet  13139  reldvg  13288  dvmptclx  13320