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

Theorem elexi 3211
Description: If a class is a member of another class, it is a set. (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 3210 . 2 (𝐴𝐵𝐴 ∈ V)
31, 2ax-mp 5 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1989  Vcvv 3198
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-12 2046  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1485  df-ex 1704  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3200
This theorem is referenced by:  onunisuci  5839  funopdmsn  6412  mptrabexOLD  6486  caovmo  6868  oev  7591  oe0  7599  oev2  7600  oneo  7658  nnneo  7728  endisj  8044  pwen  8130  sdom1  8157  1sdom  8160  cnfcom2  8596  cnfcom3lem  8597  cnfcom3  8598  rankxplim3  8741  pm54.43  8823  mappwen  8932  cda1dif  8995  pm110.643  8996  infcda1  9012  infmap2  9037  ackbij1lem5  9043  cfsuc  9076  isfin4-3  9134  dcomex  9266  pwcfsdom  9402  cfpwsdom  9403  alephom  9404  canthp1lem2  9472  pwxpndom2  9484  inar1  9594  indpi  9726  pinq  9746  archnq  9799  prlem934  9852  0idsr  9915  recexsrlem  9921  supsrlem  9929  opelreal  9948  elreal  9949  elreal2  9950  eqresr  9955  axmulass  9975  ax1ne0  9978  c0ex  10031  1ex  10032  pnfex  10090  2ex  11089  3ex  11093  elxr  11947  xnegex  12036  xaddval  12051  xmulval  12053  om2uzrdg  12750  hashxplem  13215  brfi1uzind  13275  brfi1uzindOLD  13281  opfi1uzindOLD  13284  caucvgr  14400  rpnnen  14950  rexpen  14951  sadcf  15169  sadcp1  15171  phimullem  15478  prmreclem6  15619  xpsc0  16214  xpsc1  16215  xpsfrnel  16217  xpsfrnel2  16219  xpsle  16235  setcepi  16732  efgval  18124  efgi1  18128  frgpuptinv  18178  dmdprdpr  18442  dprdpr  18443  coe1fval3  19572  00ply1bas  19604  ply1plusgfvi  19606  coe1z  19627  coe1mul2  19633  coe1tm  19637  cnfldfun  19752  cnfldfunALT  19753  xpstopnlem1  21606  xpstopnlem2  21608  xpsdsval  22180  dscmet  22371  dscopn  22372  icopnfhmeo  22736  iccpnfhmeo  22738  xrhmeo  22739  bndth  22751  mbfimaopnlem  23416  dvef  23737  mdegcl  23823  pige3  24263  cxpval  24404  1cubr  24563  emcllem7  24722  basellem7  24807  prmorcht  24898  sqff1o  24902  ppiublem2  24922  lgsval  25020  lgsdir2lem3  25046  axlowdimlem4  25819  axlowdimlem6  25821  axlowdimlem8  25823  axlowdimlem9  25824  upgrbi  25982  usgrexmpllem  26146  uhgr3cyclex  27035  konigsberglem1  27107  konigsberglem2  27108  konigsberglem3  27109  ex-opab  27273  ex-eprel  27274  ex-id  27275  ex-xp  27277  ex-cnv  27278  ex-dm  27280  ex-rn  27281  ex-res  27282  ex-fv  27284  ex-1st  27285  ex-2nd  27286  hhph  28019  hlim0  28076  hsn0elch  28089  elch0  28095  hhssabloilem  28102  choc0  28169  shintcli  28172  shincli  28205  chincli  28303  h1deoi  28392  h1de2bi  28397  h1de2ctlem  28398  spansni  28400  df0op2  28595  ho01i  28671  nmop0h  28834  opsqrlem2  28984  opsqrlem4  28986  opsqrlem5  28987  hmopidmchi  28994  atoml2i  29226  xrge0iifhmeo  29967  rezh  30000  rrhre  30050  sxbrsigalem5  30335  carsgclctunlem2  30366  ballotth  30584  cxpcncf1  30658  reprsuc  30678  reprlt  30682  reprgt  30684  circlemethnat  30704  circlevma  30705  bnj1015  31016  subfacp1lem3  31149  subfacp1lem5  31151  kur14lem7  31179  kur14lem9  31181  mrsubcv  31392  mrsubrn  31395  mvhf1  31441  msubvrs  31442  nofv  31794  sltres  31799  noxp1o  31800  noextend  31803  noextendlt  31806  noextendgt  31807  nolesgn2ores  31809  bdayfo  31812  nosepnelem  31814  nosep1o  31816  nosepdmlem  31817  nolt02o  31829  nosupno  31833  nosupbday  31835  nosupbnd1lem3  31840  nosupbnd1lem5  31842  nosupbnd1  31844  nosupbnd2lem1  31845  nosupbnd2  31846  noetalem1  31847  noetalem3  31849  noetalem4  31850  onsucsuccmpi  32426  finxpreclem2  33207  poimirlem26  33415  poimirlem27  33416  poimir  33422  mbfresfi  33436  fdc  33521  rabren3dioph  37205  pw2f1ocnv  37430  cllem0  37697  rclexi  37748  trclexi  37753  rtrclexi  37754  frege54cor1c  38035  dffrege76  38059  frege83  38066  frege97  38080  frege98  38081  dffrege99  38082  frege104  38087  frege109  38092  frege110  38093  frege131  38114  frege133  38116  clsk3nimkb  38164  clsk1indlem4  38168  clsk1indlem1  38169  clsk1independent  38170  rpex  39381  xrlexaddrp  39387  limsup10exlem  39804  limsup10ex  39805  cxpcncf2  39882  wallispilem2  40052  stirlinglem14  40073  fourierdlem70  40162  fourierdlem83  40175  fourierdlem102  40194  fourierdlem103  40195  fourierdlem104  40196  fourierdlem114  40206  fouriersw  40217  sge0tsms  40366  omeunle  40499  0ome  40512  ovn0lem  40548  hoidmvlelem3  40580  ovnhoilem1  40584  vonicclem2  40667  mbfresmf  40717  smfpimcclem  40782
  Copyright terms: Public domain W3C validator