ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elexd Unicode version

Theorem elexd 2750
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
StepHypRef Expression
1 elexd.1 . 2  |-  ( ph  ->  A  e.  V )
2 elex 2748 . 2  |-  ( A  e.  V  ->  A  e.  _V )
31, 2syl 14 1  |-  ( ph  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 2148   _Vcvv 2737
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2739
This theorem is referenced by:  ifexd  4480  dmmptd  5341  tfr1onlemsucfn  6334  tfrcllemsucfn  6347  frecrdg  6402  unsnfidcel  6913  fnfi  6929  caseinl  7083  caseinr  7084  omniwomnimkv  7158  nninfdcinf  7162  acfun  7199  seq3val  10431  seqvalcd  10432  hashennn  10731  lcmval  12033  hashdvds  12191  ennnfonelemp1  12377  isstruct2r  12443  strnfvnd  12452  strfvssn  12454  strslfv2d  12474  setsslid  12482  basmex  12490  basmexd  12491  ressbas2d  12497  ressval3d  12500  ismgmn0  12656  ismhm  12730  0mhm  12750  mulgval  12862  mulgfng  12863  mulg1  12866  mulgnnp1  12867  mulgnndir  12887  issrg  12961  ringidss  13025  ringpropd  13030  dvdsrvald  13074  dvdsrd  13075  isunitd  13087  invrfvald  13103  istopon  13144  istps  13163  tgclb  13198  restbasg  13301  restco  13307  lmfval  13325  cnfval  13327  cnpfval  13328  cnpval  13331  txcnp  13404  txrest  13409  ismet2  13487  xmetpsmet  13502  mopnval  13575  comet  13632  reldvg  13781  dvmptclx  13813
  Copyright terms: Public domain W3C validator