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  7432  caseinr  7433  omniwomnimkv  7508  nninfdcinf  7512  acfun  7564  seq3val  10912  seqvalcd  10913  seqf1oglem2  10972  seqf1og  10973  hashennn  11235  wrdexg  11331  lswex  11372  ccatw2s1leng  11422  ccat2s1fvwd  11431  swrdspsleq  11455  cats1un  11509  cats1fvd  11554  s3fv0g  11579  s3fv1g  11580  s3fv2g  11581  s1s3d  11583  s1s4d  11584  s1s5d  11585  s1s6d  11586  s1s7d  11587  s2s2d  11588  s4s2d  11589  s4s3d  11590  s3s4d  11591  s2s5d  11592  s5s2d  11593  s4s4d  11594  lcmval  12860  ballotfilemsv  13305  ennnfonelemp1  13349  isstruct2r  13415  strnfvnd  13424  strfvssn  13426  strslfv2d  13447  setsslid  13455  basmex  13464  basmexd  13465  ressbas2d  13475  ressval3d  13479  imasival  13680  imasbas  13681  imasplusg  13682  imasmulr  13683  imasaddfn  13691  imasaddval  13692  imasaddf  13693  imasmulfn  13694  imasmulval  13695  imasmulf  13696  qusval  13697  qusaddflemg  13708  qusaddval  13709  qusaddf  13710  qusmulval  13711  qusmulf  13712  xpsfrnel  13718  ismgmn0  13731  gzsumvalx  13762  gzsumfzval  13764  gzsumval2  13767  ress0g  13809  ismhm  13821  mhmex  13822  0mhm  13846  qusgrp2  13969  mulgval  13978  mulgfng  13980  mulg1  13985  mulgnnp1  13986  mulgnndir  14007  issubg2m  14045  1nsgtrivd  14075  eqgval  14079  eqgen  14083  gsumvalfi  14236  prdsex  14263  prdsval  14264  prdsbaslemss  14265  prdssgrpd  14282  prdsidlem  14284  prdsmndd  14285  prds0g  14286  prdsgrpd  14288  prdsinvgd  14289  xpsval  14292  mgpplusg  14313  mgpbas  14316  rngpropd  14345  qusrng  14348  ringidval  14356  issrg  14360  ringidss  14425  ringpropd  14434  qusring2  14462  opprringb  14477  dvdsrvald  14491  dvdsrd  14492  isunitd  14504  invrfvald  14520  dvrfvald  14531  rdivmuldivd  14542  invrpropdg  14547  isrim0  14559  rhmunitinv  14576  subrgintm  14642  rrgmex  14660  aprval  14682  aprprop  14692  lssmex  14783  islss3  14807  sraval  14865  sralemg  14866  srascag  14870  sravscag  14871  sraipg  14872  sraex  14874  lidlmex  14903  lidlrsppropdg  14923  2idlmex  14929  qusrhm  14956  zrhval  15043  asclfval  15112  psrval  15141  psrbasg  15157  psrplusgg  15161  psraddcl  15163  psrmulrg  15165  psrmulclfilem  15168  psr0cl  15170  psr0lid  15171  psrnegcl  15172  psrlinv  15173  psrgrp  15174  psr1clfi  15177  psrlidmfi  15178  mplsubgfilemcl  15189  istopon  15213  istps  15232  tgclb  15265  restbasg  15368  restco  15374  lmfval  15393  cnfval  15394  cnpfval  15395  cnpval  15398  txcnp  15471  txrest  15476  ismet2  15554  xmetpsmet  15569  mopnval  15642  comet  15699  reldvg  15879  dvmptclx  15918  lgseisenlem2  16369  1vgrex  16440  p1evtxdeqfilem  16731  p1evtxdeqfi  16732  p1evtxdp1fi  16733  upgriswlkdc  16780  eupth2lem3fi  16896  eupth2lembfi  16897