Theorem elexd 2752

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

Syntax hints:   → wi 4   ∈ wcel 2148  Vcvv 2739

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2741

This theorem is referenced by:  ifexd  4486  dmmptd  5348  tfr1onlemsucfn  6343  tfrcllemsucfn  6356  frecrdg  6411  unsnfidcel  6922  fnfi  6938  caseinl  7092  caseinr  7093  omniwomnimkv  7167  nninfdcinf  7171  acfun  7208  seq3val  10460  seqvalcd  10461  hashennn  10762  lcmval  12065  hashdvds  12223  ennnfonelemp1  12409  isstruct2r  12475  strnfvnd  12484  strfvssn  12486  strslfv2d  12507  setsslid  12515  basmex  12523  basmexd  12524  ressbas2d  12530  ressval3d  12533  prdsex  12723  imasival  12732  imasbas  12733  imasplusg  12734  imasmulr  12735  imasaddfn  12743  imasaddval  12744  imasaddf  12745  imasmulfn  12746  imasmulval  12747  imasmulf  12748  qusval  12749  qusaddflemg  12758  qusaddval  12759  qusaddf  12760  qusmulval  12761  qusmulf  12762  xpsfrnel  12768  xpsval  12776  ismgmn0  12782  ress0g  12849  ismhm  12858  0mhm  12878  mulgval  12991  mulgfng  12992  mulg1  12995  mulgnnp1  12996  mulgnndir  13017  issubg2m  13054  1nsgtrivd  13084  eqgval  13087  eqgen  13091  issrg  13153  ringidss  13217  ringpropd  13222  dvdsrvald  13267  dvdsrd  13268  isunitd  13280  invrfvald  13296  dvrfvald  13307  rdivmuldivd  13318  invrpropdg  13323  subrgintm  13369  aprval  13377  islss3  13471  istopon  13598  istps  13617  tgclb  13650  restbasg  13753  restco  13759  lmfval  13777  cnfval  13779  cnpfval  13780  cnpval  13783  txcnp  13856  txrest  13861  ismet2  13939  xmetpsmet  13954  mopnval  14027  comet  14084  reldvg  14233  dvmptclx  14265  lgseisenlem2  14536