Theorem elexd 2827

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

Syntax hints:   → wi 4   ∈ wcel 2203  Vcvv 2813

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-v 2815

This theorem is referenced by:  ifexd  4605  dmmptd  5489  mptsuppd  6456  suppssfvg  6463  tfr1onlemsucfn  6571  tfrcllemsucfn  6584  frecrdg  6639  mapsnend  7052  mapunen  7104  unsnfidcel  7181  fnfi  7203  caseinl  7382  caseinr  7383  omniwomnimkv  7458  nninfdcinf  7462  acfun  7514  seq3val  10822  seqvalcd  10823  seqf1oglem2  10882  seqf1og  10883  hashennn  11143  wrdexg  11235  lswex  11276  ccatw2s1leng  11326  ccat2s1fvwd  11335  swrdspsleq  11359  cats1un  11413  cats1fvd  11458  s3fv0g  11483  s3fv1g  11484  s3fv2g  11485  s1s3d  11487  s1s4d  11488  s1s5d  11489  s1s6d  11490  s1s7d  11491  s2s2d  11492  s4s2d  11493  s4s3d  11494  s3s4d  11495  s2s5d  11496  s5s2d  11497  s4s4d  11498  lcmval  12760  ennnfonelemp1  13157  isstruct2r  13223  strnfvnd  13232  strfvssn  13234  strslfv2d  13255  setsslid  13263  basmex  13272  basmexd  13273  ressbas2d  13281  ressval3d  13285  prdsex  13482  prdsval  13486  prdsbaslemss  13487  imasival  13519  imasbas  13520  imasplusg  13521  imasmulr  13522  imasaddfn  13530  imasaddval  13531  imasaddf  13532  imasmulfn  13533  imasmulval  13534  imasmulf  13535  qusval  13536  qusaddflemg  13547  qusaddval  13548  qusaddf  13549  qusmulval  13550  qusmulf  13551  xpsfrnel  13557  xpsval  13565  ismgmn0  13571  igsumvalx  13602  gsumfzval  13604  gsumval2  13610  prdssgrpd  13628  ress0g  13656  prdsidlem  13660  prdsmndd  13661  prds0g  13662  ismhm  13674  mhmex  13675  0mhm  13699  prdsgrpd  13822  prdsinvgd  13823  qusgrp2  13830  mulgval  13839  mulgfng  13841  mulg1  13846  mulgnnp1  13847  mulgnndir  13868  issubg2m  13906  1nsgtrivd  13936  eqgval  13940  eqgen  13944  rngpropd  14099  qusrng  14102  issrg  14109  ringidss  14173  ringpropd  14182  qusring2  14210  dvdsrvald  14238  dvdsrd  14239  isunitd  14251  invrfvald  14267  dvrfvald  14278  rdivmuldivd  14289  invrpropdg  14294  isrim0  14306  rhmunitinv  14323  subrgintm  14388  rrgmex  14406  aprval  14428  lssmex  14503  islss3  14527  sraval  14585  sralemg  14586  srascag  14590  sravscag  14591  sraipg  14592  sraex  14594  lidlmex  14623  lidlrsppropdg  14643  2idlmex  14649  qusrhm  14676  zrhval  14765  psrval  14814  psrbasg  14829  psrplusgg  14833  psraddcl  14835  psr0cl  14836  psr0lid  14837  psrnegcl  14838  psrlinv  14839  psrgrp  14840  psr1clfi  14843  mplsubgfilemcl  14854  istopon  14878  istps  14897  tgclb  14930  restbasg  15033  restco  15039  lmfval  15058  cnfval  15059  cnpfval  15060  cnpval  15063  txcnp  15136  txrest  15141  ismet2  15219  xmetpsmet  15234  mopnval  15307  comet  15364  reldvg  15544  dvmptclx  15583  lgseisenlem2  15944  1vgrex  16015  p1evtxdeqfilem  16306  p1evtxdeqfi  16307  p1evtxdp1fi  16308  upgriswlkdc  16355  eupth2lem3fi  16471  eupth2lembfi  16472  gfsumval  16862