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

Theorem elexi 3181
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 3180 . 2 (𝐴𝐵𝐴 ∈ V)
31, 2ax-mp 5 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1975  Vcvv 3168
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-12 2031  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-v 3170
This theorem is referenced by:  onunisuci  5740  mptrabexOLD  6367  caovmo  6742  oev  7454  oe0  7462  oev2  7463  oneo  7521  nnneo  7591  endisj  7905  pwen  7991  sdom1  8018  1sdom  8021  cnfcom2  8455  cnfcom3lem  8456  cnfcom3  8457  rankxplim3  8600  pm54.43  8682  mappwen  8791  cda1dif  8854  pm110.643  8855  infcda1  8871  infmap2  8896  ackbij1lem5  8902  cfsuc  8935  isfin4-3  8993  dcomex  9125  pwcfsdom  9257  cfpwsdom  9258  alephom  9259  canthp1lem2  9327  pwxpndom2  9339  inar1  9449  indpi  9581  pinq  9601  archnq  9654  prlem934  9707  0idsr  9770  recexsrlem  9776  supsrlem  9784  opelreal  9803  elreal  9804  elreal2  9805  eqresr  9810  axmulass  9830  ax1ne0  9833  c0ex  9886  1ex  9887  2ex  10935  3ex  10939  pnfex  11778  elxr  11781  xnegex  11868  xaddval  11883  xmulval  11885  om2uzrdg  12568  hashxplem  13028  brfi1uzind  13077  opfi1uzind  13080  brfi1uzindOLD  13083  opfi1uzindOLD  13086  caucvgr  14196  rpnnen  14737  rexpen  14738  sadcf  14955  sadcp1  14957  phimullem  15264  prmreclem6  15405  xpsc0  15985  xpsc1  15986  xpsfrnel  15988  xpsfrnel2  15990  xpsle  16006  setcepi  16503  efgval  17895  efgi1  17899  frgpuptinv  17949  dmdprdpr  18213  dprdpr  18214  coe1fval3  19341  00ply1bas  19373  ply1plusgfvi  19375  coe1z  19396  coe1mul2  19402  coe1tm  19406  xpstopnlem1  21360  xpstopnlem2  21362  xpsdsval  21933  dscmet  22124  dscopn  22125  icopnfhmeo  22477  iccpnfhmeo  22479  xrhmeo  22480  bndth  22492  mbfimaopnlem  23141  dvef  23460  mdegcl  23546  pige3  23986  cxpval  24123  1cubr  24282  emcllem7  24441  basellem7  24526  prmorcht  24617  sqff1o  24621  ppiublem2  24641  lgsval  24739  lgsdir2lem3  24765  axlowdimlem4  25539  axlowdimlem6  25541  axlowdimlem8  25543  axlowdimlem9  25544  usgraexmpl  25692  usgra2adedgwlkonALT  25906  umgrabi  26272  ex-opab  26443  ex-eprel  26444  ex-id  26445  ex-xp  26447  ex-cnv  26448  ex-dm  26450  ex-rn  26451  ex-res  26452  ex-fv  26454  ex-1st  26455  ex-2nd  26456  hhph  27221  hlim0  27278  hsn0elch  27291  elch0  27297  hhssabloilem  27304  choc0  27371  shintcli  27374  shincli  27407  chincli  27505  h1deoi  27594  h1de2bi  27599  h1de2ctlem  27600  spansni  27602  df0op2  27797  ho01i  27873  nmop0h  28036  opsqrlem2  28186  opsqrlem4  28188  opsqrlem5  28189  hmopidmchi  28196  atoml2i  28428  xrge0iifhmeo  29112  rezh  29145  rrhre  29195  sxbrsigalem5  29479  carsgclctunlem2  29510  ballotth  29728  bnj1015  30087  subfacp1lem3  30220  subfacp1lem5  30222  kur14lem7  30250  kur14lem9  30252  mrsubcv  30463  mrsubrn  30466  mvhf1  30512  msubvrs  30513  nofv  30856  sltres  30863  noxp1o  30865  noxp2o  30866  bdayfo  30876  nobndlem3  30895  nobndlem7  30899  nobndup  30901  nobnddown  30902  onsucsuccmpi  31414  finxpreclem2  32202  poimirlem26  32404  poimirlem27  32405  poimir  32411  mbfresfi  32425  fdc  32510  rabren3dioph  36196  pw2f1ocnv  36421  cllem0  36689  rclexi  36740  trclexi  36745  rtrclexi  36746  frege54cor1c  37028  dffrege76  37052  frege83  37059  frege97  37073  frege98  37074  dffrege99  37075  frege104  37080  frege109  37085  frege110  37086  frege131  37107  frege133  37109  clsk3nimkb  37157  clsk1indlem4  37161  clsk1indlem1  37162  clsk1independent  37163  rpex  38303  xrlexaddrp  38309  cxpcncf2  38586  wallispilem2  38759  stirlinglem14  38780  fourierdlem70  38869  fourierdlem83  38882  fourierdlem102  38901  fourierdlem103  38902  fourierdlem104  38903  fourierdlem114  38913  fouriersw  38924  sge0tsms  39073  omeunle  39206  0ome  39219  ovn0lem  39255  hoidmvlelem3  39287  ovnhoilem1  39291  vonicclem2  39375  mbfresmf  39426  structvtxval  40252  structiedg0val  40253  upgrbi  40317  usgrexmpllem  40482  1wlk2v2e  41322  uhgr3cyclex  41347  konigsberglem1  41420  konigsberglem2  41421  konigsberglem3  41422
  Copyright terms: Public domain W3C validator