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

Theorem elexd 2673
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 2671 . 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 1465   _Vcvv 2660
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-v 2662
This theorem is referenced by:  dmmptd  5223  tfr1onlemsucfn  6205  tfrcllemsucfn  6218  frecrdg  6273  unsnfidcel  6777  fnfi  6793  caseinl  6944  caseinr  6945  acfun  7031  seq3val  10199  seqvalcd  10200  hashennn  10494  lcmval  11671  hashdvds  11824  ennnfonelemp1  11846  isstruct2r  11897  strnfvnd  11906  strfvssn  11908  strslfv2d  11928  setsslid  11936  ressid2  11945  ressval2  11946  istopon  12107  istps  12126  tgclb  12161  restbasg  12264  restco  12270  lmfval  12288  cnfval  12290  cnpfval  12291  cnpval  12294  txcnp  12367  txrest  12372  ismet2  12450  xmetpsmet  12465  mopnval  12538  comet  12595  reldvg  12744  dvmptclx  12776
  Copyright terms: Public domain W3C validator