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

Theorem elexd 2725
 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 (𝜑𝐴 ∈ V)

Proof of Theorem elexd
StepHypRef Expression
1 elexd.1 . 2 (𝜑𝐴𝑉)
2 elex 2723 . 2 (𝐴𝑉𝐴 ∈ V)
31, 2syl 14 1 (𝜑𝐴 ∈ V)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 2128  Vcvv 2712 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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2139 This theorem depends on definitions:  df-bi 116  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-v 2714 This theorem is referenced by:  ifexd  4442  dmmptd  5297  tfr1onlemsucfn  6281  tfrcllemsucfn  6294  frecrdg  6349  unsnfidcel  6858  fnfi  6874  caseinl  7025  caseinr  7026  omniwomnimkv  7093  acfun  7125  seq3val  10339  seqvalcd  10340  hashennn  10636  lcmval  11920  hashdvds  12073  ennnfonelemp1  12107  isstruct2r  12161  strnfvnd  12170  strfvssn  12172  strslfv2d  12192  setsslid  12200  ressid2  12209  ressval2  12210  istopon  12371  istps  12390  tgclb  12425  restbasg  12528  restco  12534  lmfval  12552  cnfval  12554  cnpfval  12555  cnpval  12558  txcnp  12631  txrest  12636  ismet2  12714  xmetpsmet  12729  mopnval  12802  comet  12859  reldvg  13008  dvmptclx  13040
 Copyright terms: Public domain W3C validator