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

Theorem elexi 3244
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 3243 . 2 (𝐴𝐵𝐴 ∈ V)
31, 2ax-mp 5 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  Vcvv 3231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1526  df-ex 1745  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233
This theorem is referenced by:  onunisuci  5879  funopdmsn  6455  caovmo  6913  oev  7639  oe0  7647  oev2  7648  oneo  7706  nnneo  7776  endisj  8088  pwen  8174  sdom1  8201  1sdom  8204  cnfcom2  8637  cnfcom3lem  8638  cnfcom3  8639  rankxplim3  8782  pm54.43  8864  mappwen  8973  cda1dif  9036  pm110.643  9037  infcda1  9053  infmap2  9078  ackbij1lem5  9084  cfsuc  9117  isfin4-3  9175  dcomex  9307  pwcfsdom  9443  cfpwsdom  9444  alephom  9445  canthp1lem2  9513  pwxpndom2  9525  inar1  9635  indpi  9767  pinq  9787  archnq  9840  prlem934  9893  0idsr  9956  recexsrlem  9962  supsrlem  9970  opelreal  9989  elreal  9990  elreal2  9991  eqresr  9996  axmulass  10016  ax1ne0  10019  c0ex  10072  1ex  10073  pnfex  10131  2ex  11130  3ex  11134  elxr  11988  xnegex  12077  xaddval  12092  xmulval  12094  om2uzrdg  12795  hashxplem  13258  brfi1uzind  13318  caucvgr  14450  rpnnen  15000  rexpen  15001  sadcf  15222  sadcp1  15224  phimullem  15531  prmreclem6  15672  xpsc0  16267  xpsc1  16268  xpsfrnel  16270  xpsfrnel2  16272  xpsle  16288  setcepi  16785  efgval  18176  efgi1  18180  frgpuptinv  18230  dmdprdpr  18494  dprdpr  18495  coe1fval3  19626  00ply1bas  19658  ply1plusgfvi  19660  coe1z  19681  coe1mul2  19687  coe1tm  19691  cnfldfun  19806  cnfldfunALT  19807  xpstopnlem1  21660  xpstopnlem2  21662  xpsdsval  22233  dscmet  22424  dscopn  22425  icopnfhmeo  22789  iccpnfhmeo  22791  xrhmeo  22792  bndth  22804  mbfimaopnlem  23467  dvef  23788  mdegcl  23874  pige3  24314  cxpval  24455  1cubr  24614  emcllem7  24773  basellem7  24858  prmorcht  24949  sqff1o  24953  ppiublem2  24973  lgsval  25071  lgsdir2lem3  25097  axlowdimlem4  25870  axlowdimlem6  25872  axlowdimlem8  25874  axlowdimlem9  25875  upgrbi  26033  usgrexmpllem  26197  clwwlknon1sn  27075  uhgr3cyclex  27160  konigsberglem1  27230  konigsberglem2  27231  konigsberglem3  27232  ex-opab  27419  ex-eprel  27420  ex-id  27421  ex-xp  27423  ex-cnv  27424  ex-dm  27426  ex-rn  27427  ex-res  27428  ex-fv  27430  ex-1st  27431  ex-2nd  27432  hhph  28163  hlim0  28220  hsn0elch  28233  elch0  28239  hhssabloilem  28246  choc0  28313  shintcli  28316  shincli  28349  chincli  28447  h1deoi  28536  h1de2bi  28541  h1de2ctlem  28542  spansni  28544  df0op2  28739  ho01i  28815  nmop0h  28978  opsqrlem2  29128  opsqrlem4  29130  opsqrlem5  29131  hmopidmchi  29138  atoml2i  29370  xrge0iifhmeo  30110  rezh  30143  rrhre  30193  sxbrsigalem5  30478  carsgclctunlem2  30509  ballotth  30727  cxpcncf1  30801  reprsuc  30821  reprlt  30825  reprgt  30827  circlemethnat  30847  circlevma  30848  bnj1015  31157  subfacp1lem3  31290  subfacp1lem5  31292  kur14lem7  31320  kur14lem9  31322  mrsubcv  31533  mrsubrn  31536  mvhf1  31582  msubvrs  31583  nofv  31935  sltres  31940  noxp1o  31941  noextend  31944  noextendlt  31947  noextendgt  31948  nolesgn2ores  31950  bdayfo  31953  nosepnelem  31955  nosep1o  31957  nosepdmlem  31958  nolt02o  31970  nosupno  31974  nosupbday  31976  nosupbnd1lem3  31981  nosupbnd1lem5  31983  nosupbnd1  31985  nosupbnd2lem1  31986  nosupbnd2  31987  noetalem1  31988  noetalem3  31990  noetalem4  31991  onsucsuccmpi  32567  finxpreclem2  33357  poimirlem26  33565  poimirlem27  33566  poimir  33572  mbfresfi  33586  fdc  33671  rabren3dioph  37696  pw2f1ocnv  37921  cllem0  38188  rclexi  38239  trclexi  38244  rtrclexi  38245  frege54cor1c  38526  dffrege76  38550  frege83  38557  frege97  38571  frege98  38572  dffrege99  38573  frege104  38578  frege109  38583  frege110  38584  frege131  38605  frege133  38607  clsk3nimkb  38655  clsk1indlem4  38659  clsk1indlem1  38660  clsk1independent  38661  rpex  39875  xrlexaddrp  39881  limsup10exlem  40322  limsup10ex  40323  cxpcncf2  40431  wallispilem2  40601  stirlinglem14  40622  fourierdlem70  40711  fourierdlem83  40724  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem114  40755  fouriersw  40766  sge0tsms  40915  omeunle  41051  0ome  41064  ovn0lem  41100  hoidmvlelem3  41132  ovnhoilem1  41136  vonicclem2  41219  mbfresmf  41269  smfpimcclem  41334
  Copyright terms: Public domain W3C validator