MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elexd Structured version   Visualization version   GIF version

Theorem elexd 3203
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 3201 . 2 (𝐴𝑉𝐴 ∈ V)
31, 2syl 17 1 (𝜑𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  Vcvv 3189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1483  df-ex 1702  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3191
This theorem is referenced by:  reuhypd  4860  ideqg  5238  elrnmptg  5340  fvmptdf  6257  pospropd  17062  gsumvalx  17198  isunit  18585  israg  25505  structtocusgr  26242  1loopgrnb0  26297  iswlkg  26392  sitgval  30193  bnj1463  30858  wsuclem  31501  rfovd  37804  fsovd  37811  fsovrfovd  37812  dssmapfvd  37820  projf1o  38883  mapsnend  38888  limsupvaluz  39367  limsupequzmpt2  39377  limsupvaluz2  39397  rrxsnicc  39848  ioorrnopnlem  39852  ioorrnopnxrlem  39854  subsaliuncl  39904  sge0xaddlem1  39978  sge0xaddlem2  39979  sge0xadd  39980  sge0splitsn  39986  meaiuninclem  40025  meaiininclem  40028  hoiprodcl2  40097  hoicvrrex  40098  ovn0lem  40107  hoidmvlelem3  40139  ovnhoilem1  40143  hoicoto2  40147  hoidifhspval3  40161  hoiqssbllem1  40164  ovolval4lem1  40191  ovnovollem2  40199  vonvolmbl  40203  iinhoiicclem  40215  iunhoiioolem  40217  vonioolem1  40222  vonioolem2  40223  vonicclem1  40225  vonicclem2  40226  decsmf  40303  smflimlem4  40310  smfmullem4  40329  smfco  40337  smfpimcclem  40341  smflimsuplem2  40355  smflimsuplem5  40358  smflimsupmpt  40363  opabresex0d  40622  setsnidel  40666  isupwlkg  41027
  Copyright terms: Public domain W3C validator