Theorem elexd 2773

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

Syntax hints:   → wi 4   ∈ wcel 2164  Vcvv 2760

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-v 2762

This theorem is referenced by:  ifexd  4516  dmmptd  5385  tfr1onlemsucfn  6395  tfrcllemsucfn  6408  frecrdg  6463  unsnfidcel  6979  fnfi  6997  caseinl  7152  caseinr  7153  omniwomnimkv  7228  nninfdcinf  7232  acfun  7269  seq3val  10534  seqvalcd  10535  seqf1oglem2  10594  seqf1og  10595  hashennn  10854  wrdexg  10928  lcmval  12204  hashdvds  12362  ennnfonelemp1  12566  isstruct2r  12632  strnfvnd  12641  strfvssn  12643  strslfv2d  12664  setsslid  12672  basmex  12680  basmexd  12681  ressbas2d  12689  ressval3d  12693  prdsex  12883  imasival  12892  imasbas  12893  imasplusg  12894  imasmulr  12895  imasaddfn  12903  imasaddval  12904  imasaddf  12905  imasmulfn  12906  imasmulval  12907  imasmulf  12908  qusval  12909  qusaddflemg  12920  qusaddval  12921  qusaddf  12922  qusmulval  12923  qusmulf  12924  xpsfrnel  12930  xpsval  12938  ismgmn0  12944  igsumvalx  12975  gsumfzval  12977  gsumval2  12983  ress0g  13027  ismhm  13036  mhmex  13037  0mhm  13061  qusgrp2  13186  mulgval  13195  mulgfng  13197  mulg1  13202  mulgnnp1  13203  mulgnndir  13224  issubg2m  13262  1nsgtrivd  13292  eqgval  13296  eqgen  13300  rngpropd  13454  qusrng  13457  issrg  13464  ringidss  13528  ringpropd  13537  qusring2  13565  dvdsrvald  13592  dvdsrd  13593  isunitd  13605  invrfvald  13621  dvrfvald  13632  rdivmuldivd  13643  invrpropdg  13648  isrim0  13660  rhmunitinv  13677  subrgintm  13742  rrgmex  13760  aprval  13781  lssmex  13854  islss3  13878  sraval  13936  sralemg  13937  srascag  13941  sravscag  13942  sraipg  13943  sraex  13945  lidlmex  13974  lidlrsppropdg  13994  2idlmex  14000  qusrhm  14027  zrhval  14116  psrval  14163  psrbasg  14170  psrplusgg  14173  psraddcl  14175  istopon  14192  istps  14211  tgclb  14244  restbasg  14347  restco  14353  lmfval  14371  cnfval  14373  cnpfval  14374  cnpval  14377  txcnp  14450  txrest  14455  ismet2  14533  xmetpsmet  14548  mopnval  14621  comet  14678  reldvg  14858  dvmptclx  14897  lgseisenlem2  15228