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

Theorem elexd 2703
 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
Assertion
Ref Expression
elexd

Proof of Theorem elexd
StepHypRef Expression
1 elexd.1 . 2
2 elex 2701 . 2
31, 2syl 14 1
 Colors of variables: wff set class Syntax hints:   wi 4   wcel 1481  cvv 2690 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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-v 2692 This theorem is referenced by:  dmmptd  5262  tfr1onlemsucfn  6246  tfrcllemsucfn  6259  frecrdg  6314  unsnfidcel  6819  fnfi  6835  caseinl  6986  caseinr  6987  omniwomnimkv  7051  acfun  7083  seq3val  10282  seqvalcd  10283  hashennn  10578  lcmval  11800  hashdvds  11953  ennnfonelemp1  11975  isstruct2r  12029  strnfvnd  12038  strfvssn  12040  strslfv2d  12060  setsslid  12068  ressid2  12077  ressval2  12078  istopon  12239  istps  12258  tgclb  12293  restbasg  12396  restco  12402  lmfval  12420  cnfval  12422  cnpfval  12423  cnpval  12426  txcnp  12499  txrest  12504  ismet2  12582  xmetpsmet  12597  mopnval  12670  comet  12727  reldvg  12876  dvmptclx  12908
 Copyright terms: Public domain W3C validator