Theorem elexd 2835

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	|- ( ph -> A e. V )

Assertion

Ref	Expression
elexd	|- ( ph -> A e. _V )

Proof of Theorem elexd

Step	Hyp	Ref	Expression
1		elexd.1	. 2 |- ( ph -> A e. V )
2		elex 2833	. 2 |- ( A e. V -> A e. _V )
3	1, 2	syl 14	1 |- ( ph -> A e. _V )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   _Vcvv 2821

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is used by:  ifexd  4630  dmmptd  5514  relndmfv  5728  mptsuppd  6496  suppssfvg  6503  tfr1onlemsucfn  6611  tfrcllemsucfn  6624  frecrdg  6679  mapsnend  7099  mapunen  7151  unsnfidcel  7228  fnfi  7250  caseinl  7431  caseinr  7432  omniwomnimkv  7507  nninfdcinf  7511  acfun  7563  seq3val  10897  seqvalcd  10898  seqf1oglem2  10957  seqf1og  10958  hashennn  11219  wrdexg  11315  lswex  11356  ccatw2s1leng  11406  ccat2s1fvwd  11415  swrdspsleq  11439  cats1un  11493  cats1fvd  11538  s3fv0g  11563  s3fv1g  11564  s3fv2g  11565  s1s3d  11567  s1s4d  11568  s1s5d  11569  s1s6d  11570  s1s7d  11571  s2s2d  11572  s4s2d  11573  s4s3d  11574  s3s4d  11575  s2s5d  11576  s5s2d  11577  s4s4d  11578  lcmval  12841  ballotfilemsv  13253  ennnfonelemp1  13297  isstruct2r  13363  strnfvnd  13372  strfvssn  13374  strslfv2d  13395  setsslid  13403  basmex  13412  basmexd  13413  ressbas2d  13422  ressval3d  13426  imasival  13627  imasbas  13628  imasplusg  13629  imasmulr  13630  imasaddfn  13638  imasaddval  13639  imasaddf  13640  imasmulfn  13641  imasmulval  13642  imasmulf  13643  qusval  13644  qusaddflemg  13655  qusaddval  13656  qusaddf  13657  qusmulval  13658  qusmulf  13659  xpsfrnel  13665  ismgmn0  13678  gzsumvalx  13709  gzsumfzval  13711  gzsumval2  13714  ress0g  13756  ismhm  13768  mhmex  13769  0mhm  13793  qusgrp2  13916  mulgval  13925  mulgfng  13927  mulg1  13932  mulgnnp1  13933  mulgnndir  13954  issubg2m  13992  1nsgtrivd  14022  eqgval  14026  eqgen  14030  gsumvalfi  14152  prdsex  14172  prdsval  14173  prdsbaslemss  14174  prdssgrpd  14191  prdsidlem  14193  prdsmndd  14194  prds0g  14195  prdsgrpd  14197  prdsinvgd  14198  xpsval  14201  mgpplusg  14222  mgpbas  14225  rngpropd  14254  qusrng  14257  ringidval  14265  issrg  14269  ringidss  14334  ringpropd  14343  qusring2  14371  opprringb  14386  dvdsrvald  14400  dvdsrd  14401  isunitd  14413  invrfvald  14429  dvrfvald  14440  rdivmuldivd  14451  invrpropdg  14456  isrim0  14468  rhmunitinv  14485  subrgintm  14551  rrgmex  14569  aprval  14591  aprprop  14601  lssmex  14692  islss3  14716  sraval  14774  sralemg  14775  srascag  14779  sravscag  14780  sraipg  14781  sraex  14783  lidlmex  14812  lidlrsppropdg  14832  2idlmex  14838  qusrhm  14865  zrhval  14952  asclfval  15021  psrval  15050  psrbasg  15065  psrplusgg  15069  psraddcl  15071  psr0cl  15072  psr0lid  15073  psrnegcl  15074  psrlinv  15075  psrgrp  15076  psr1clfi  15079  mplsubgfilemcl  15090  istopon  15114  istps  15133  tgclb  15166  restbasg  15269  restco  15275  lmfval  15294  cnfval  15295  cnpfval  15296  cnpval  15299  txcnp  15372  txrest  15377  ismet2  15455  xmetpsmet  15470  mopnval  15543  comet  15600  reldvg  15780  dvmptclx  15819  lgseisenlem2  16190  1vgrex  16261  p1evtxdeqfilem  16552  p1evtxdeqfi  16553  p1evtxdp1fi  16554  upgriswlkdc  16601  eupth2lem3fi  16717  eupth2lembfi  16718