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

Theorem elexi 3514
Description: If a class is a member of another class, then it is a set. Inference associated with elex 3513. (Contributed by NM, 11-Jun-1994.)
Hypothesis
Ref Expression
elexi.1 𝐴𝐵
Assertion
Ref Expression
elexi 𝐴 ∈ V

Proof of Theorem elexi
StepHypRef Expression
1 elexi.1 . 2 𝐴𝐵
2 elex 3513 . 2 (𝐴𝐵𝐴 ∈ V)
31, 2ax-mp 5 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  Vcvv 3495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-v 3497
This theorem is referenced by:  onunisuci  6298  funopdmsn  6905  caovmo  7374  1oex  8101  pwen  8679  cnfcom2  9154  cnfcom3lem  9155  cnfcom3  9156  rankxplim3  9299  mappwen  9527  ackbij1lem5  9635  alephom  9996  inar1  10186  prlem934  10444  0idsr  10508  recexsrlem  10514  supsrlem  10522  opelreal  10541  elreal  10542  elreal2  10543  eqresr  10548  axmulass  10568  ax1ne0  10571  c0ex  10624  1ex  10626  2ex  11703  3ex  11708  elxr  12501  xnegex  12591  xaddval  12606  xmulval  12608  om2uzrdg  13314  hashxplem  13784  caucvgr  15022  rpnnen  15570  rexpen  15571  phimullem  16106  prmreclem6  16247  efgval  18774  coe1mul2  20367  cnfldfun  20487  cnfldfunALT  20488  dscmet  23111  dscopn  23112  icopnfhmeo  23476  iccpnfhmeo  23478  xrhmeo  23479  bndth  23491  mbfimaopnlem  24185  mdegcl  24592  pige3ALT  25034  cxpval  25174  1cubr  25347  emcllem7  25507  basellem7  25592  prmorcht  25683  sqff1o  25687  ppiublem2  25707  lgsval  25805  lgsdir2lem3  25831  axlowdimlem4  26659  axlowdimlem6  26661  upgrbi  26806  usgrexmpllem  26970  clwwlknon1sn  27807  uhgr3cyclex  27889  konigsberglem1  27959  konigsberglem2  27960  konigsberglem3  27961  ex-opab  28139  ex-eprel  28140  ex-id  28141  ex-xp  28143  ex-cnv  28144  ex-dm  28146  ex-rn  28147  ex-res  28148  ex-fv  28150  ex-1st  28151  ex-2nd  28152  hhph  28883  hlim0  28940  hsn0elch  28953  elch0  28959  hhssabloilem  28966  choc0  29031  shintcli  29034  shincli  29067  chincli  29165  h1deoi  29254  h1de2bi  29259  h1de2ctlem  29260  spansni  29262  df0op2  29457  ho01i  29533  nmop0h  29696  opsqrlem2  29846  opsqrlem4  29848  opsqrlem5  29849  hmopidmchi  29856  atoml2i  30088  s3clhash  30552  xrge0iifhmeo  31079  rezh  31112  rrhre  31162  sxbrsigalem5  31446  carsgclctunlem2  31477  ballotth  31695  reprsuc  31786  reprlt  31790  reprgt  31792  circlemethnat  31812  circlevma  31813  bnj1015  32133  subfacp1lem3  32327  subfacp1lem5  32329  kur14lem7  32357  kur14lem9  32359  mrsubcv  32655  mrsubrn  32658  mvhf1  32704  msubvrs  32705  nofv  33062  sltres  33067  noextend  33071  noextendgt  33075  nolesgn2ores  33077  nosepnelem  33082  nosepdmlem  33085  nolt02o  33097  nosupno  33101  nosupbday  33103  nosupbnd1lem3  33108  nosupbnd1  33112  nosupbnd2lem1  33113  nosupbnd2  33114  onsucsuccmpi  33689  finxpreclem2  34554  poimirlem26  34800  poimirlem27  34801  poimir  34807  mbfresfi  34820  fdc  34903  rabren3dioph  39292  cllem0  39805  rclexi  39855  trclexi  39860  rtrclexi  39861  frege54cor1c  40141  dffrege76  40165  frege83  40172  frege97  40186  frege98  40187  dffrege99  40188  frege104  40193  frege109  40198  frege110  40199  frege131  40220  frege133  40222  clsk1independent  40276  rpex  41494  xrlexaddrp  41500  limsup10exlem  41933  limsup10ex  41934  wallispilem2  42232  stirlinglem14  42253  fourierdlem70  42342  fourierdlem83  42355  fourierdlem102  42374  fourierdlem103  42375  fourierdlem104  42376  fourierdlem114  42386  fouriersw  42397  sge0tsms  42543  omeunle  42679  0ome  42692  ovn0lem  42728  hoidmvlelem3  42760  ovnhoilem1  42764  vonicclem2  42847  mbfresmf  42897  smfpimcclem  42962  nfermltl8rev  43754  nfermltlrev  43756
  Copyright terms: Public domain W3C validator