Theorem elexd 2813

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 2811	. 2 |- ( A e. V -> A e. _V )
3	1, 2	syl 14	1 |- ( ph -> A e. _V )

Syntax hints:   -> wi 4   e. wcel 2200   _Vcvv 2799

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2801

This theorem is referenced by:  ifexd  4575  dmmptd  5454  tfr1onlemsucfn  6492  tfrcllemsucfn  6505  frecrdg  6560  unsnfidcel  7094  fnfi  7114  caseinl  7269  caseinr  7270  omniwomnimkv  7345  nninfdcinf  7349  acfun  7400  seq3val  10694  seqvalcd  10695  seqf1oglem2  10754  seqf1og  10755  hashennn  11014  wrdexg  11095  lswex  11136  swrdspsleq  11215  cats1un  11269  cats1fvd  11314  s3fv0g  11339  s3fv1g  11340  lcmval  12601  hashdvds  12759  ennnfonelemp1  12993  isstruct2r  13059  strnfvnd  13068  strfvssn  13070  strslfv2d  13091  setsslid  13099  basmex  13108  basmexd  13109  ressbas2d  13117  ressval3d  13121  prdsex  13318  prdsval  13322  prdsbaslemss  13323  imasival  13355  imasbas  13356  imasplusg  13357  imasmulr  13358  imasaddfn  13366  imasaddval  13367  imasaddf  13368  imasmulfn  13369  imasmulval  13370  imasmulf  13371  qusval  13372  qusaddflemg  13383  qusaddval  13384  qusaddf  13385  qusmulval  13386  qusmulf  13387  xpsfrnel  13393  xpsval  13401  ismgmn0  13407  igsumvalx  13438  gsumfzval  13440  gsumval2  13446  prdssgrpd  13464  ress0g  13492  prdsidlem  13496  prdsmndd  13497  prds0g  13498  ismhm  13510  mhmex  13511  0mhm  13535  prdsgrpd  13658  prdsinvgd  13659  qusgrp2  13666  mulgval  13675  mulgfng  13677  mulg1  13682  mulgnnp1  13683  mulgnndir  13704  issubg2m  13742  1nsgtrivd  13772  eqgval  13776  eqgen  13780  rngpropd  13934  qusrng  13937  issrg  13944  ringidss  14008  ringpropd  14017  qusring2  14045  dvdsrvald  14073  dvdsrd  14074  isunitd  14086  invrfvald  14102  dvrfvald  14113  rdivmuldivd  14124  invrpropdg  14129  isrim0  14141  rhmunitinv  14158  subrgintm  14223  rrgmex  14241  aprval  14262  lssmex  14335  islss3  14359  sraval  14417  sralemg  14418  srascag  14422  sravscag  14423  sraipg  14424  sraex  14426  lidlmex  14455  lidlrsppropdg  14475  2idlmex  14481  qusrhm  14508  zrhval  14597  psrval  14646  psrbasg  14654  psrplusgg  14658  psraddcl  14660  psr0cl  14661  psr0lid  14662  psrnegcl  14663  psrlinv  14664  psrgrp  14665  psr1clfi  14668  mplsubgfilemcl  14679  istopon  14703  istps  14722  tgclb  14755  restbasg  14858  restco  14864  lmfval  14883  cnfval  14884  cnpfval  14885  cnpval  14888  txcnp  14961  txrest  14966  ismet2  15044  xmetpsmet  15059  mopnval  15132  comet  15189  reldvg  15369  dvmptclx  15408  lgseisenlem2  15766  1vgrex  15837  upgriswlkdc  16106