Theorem elexd 2765

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

Syntax hints:   -> wi 4   e. wcel 2160   _Vcvv 2752

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 2171

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-v 2754

This theorem is referenced by:  ifexd  4502  dmmptd  5365  tfr1onlemsucfn  6366  tfrcllemsucfn  6379  frecrdg  6434  unsnfidcel  6950  fnfi  6967  caseinl  7121  caseinr  7122  omniwomnimkv  7196  nninfdcinf  7200  acfun  7237  seq3val  10491  seqvalcd  10492  hashennn  10795  lcmval  12098  hashdvds  12256  ennnfonelemp1  12460  isstruct2r  12526  strnfvnd  12535  strfvssn  12537  strslfv2d  12558  setsslid  12566  basmex  12574  basmexd  12575  ressbas2d  12583  ressval3d  12587  prdsex  12777  imasival  12786  imasbas  12787  imasplusg  12788  imasmulr  12789  imasaddfn  12797  imasaddval  12798  imasaddf  12799  imasmulfn  12800  imasmulval  12801  imasmulf  12802  qusval  12803  qusaddflemg  12813  qusaddval  12814  qusaddf  12815  qusmulval  12816  qusmulf  12817  xpsfrnel  12823  xpsval  12831  ismgmn0  12837  igsumvalx  12868  gsumval2  12875  ress0g  12919  ismhm  12928  mhmex  12929  0mhm  12953  qusgrp2  13070  mulgval  13079  mulgfng  13081  mulg1  13086  mulgnnp1  13087  mulgnndir  13108  issubg2m  13145  1nsgtrivd  13175  eqgval  13179  eqgen  13183  rngpropd  13326  qusrng  13329  issrg  13336  ringidss  13400  ringpropd  13409  qusring2  13433  dvdsrvald  13460  dvdsrd  13461  isunitd  13473  invrfvald  13489  dvrfvald  13500  rdivmuldivd  13511  invrpropdg  13516  isrim0  13528  rhmunitinv  13545  subrgintm  13607  aprval  13615  lssmex  13688  islss3  13712  sraval  13770  sralemg  13771  srascag  13775  sravscag  13776  sraipg  13777  sraex  13779  lidlmex  13808  lidlrsppropdg  13828  2idlmex  13835  psrval  13961  psrbasg  13968  psrplusgg  13971  psraddcl  13973  istopon  13990  istps  14009  tgclb  14042  restbasg  14145  restco  14151  lmfval  14169  cnfval  14171  cnpfval  14172  cnpval  14175  txcnp  14248  txrest  14253  ismet2  14331  xmetpsmet  14346  mopnval  14419  comet  14476  reldvg  14625  dvmptclx  14657  lgseisenlem2  14929