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

Theorem elexi 3418
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 3417 . 2 (𝐴𝐵𝐴 ∈ V)
31, 2ax-mp 5 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2157  Vcvv 3402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-12 2215  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-tru 1641  df-ex 1860  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-v 3404
This theorem is referenced by:  onunisuci  6064  funopdmsn  6649  caovmo  7111  1oex  7814  nnneo  7978  pwen  8382  1sdom  8412  cnfcom2  8856  cnfcom3lem  8857  cnfcom3  8858  rankxplim3  9001  djurcl  9030  djurf1o  9032  djuun  9045  mappwen  9228  pm110.643  9294  infmap2  9335  ackbij1lem5  9341  cfpwsdom  9701  alephom  9702  canthp1lem2  9770  inar1  9892  indpi  10024  pinq  10044  archnq  10097  prlem934  10150  0idsr  10213  recexsrlem  10219  supsrlem  10227  opelreal  10246  elreal  10247  elreal2  10248  eqresr  10253  axmulass  10273  ax1ne0  10276  c0ex  10329  1ex  10331  pnfex  10388  2ex  11390  3ex  11396  elxr  12186  xnegex  12277  xaddval  12292  xmulval  12294  om2uzrdg  12999  hashxplem  13457  brfi1uzind  13517  caucvgr  14649  rpnnen  15196  rexpen  15197  phimullem  15721  prmreclem6  15862  setcepi  16962  efgval  18351  coe1mul2  19867  cnfldfun  19986  cnfldfunALT  19987  dscmet  22611  dscopn  22612  icopnfhmeo  22976  iccpnfhmeo  22978  xrhmeo  22979  bndth  22991  mbfimaopnlem  23659  dvef  23980  mdegcl  24066  pige3  24507  cxpval  24647  1cubr  24806  emcllem7  24965  basellem7  25050  prmorcht  25141  sqff1o  25145  ppiublem2  25165  lgsval  25263  lgsdir2lem3  25289  axlowdimlem4  26062  axlowdimlem6  26064  axlowdimlem8  26066  axlowdimlem9  26067  upgrbi  26225  usgrexmpllem  26391  clwwlknon1sn  27291  uhgr3cyclex  27378  konigsberglem1  27448  konigsberglem2  27449  konigsberglem3  27450  ex-opab  27643  ex-eprel  27644  ex-id  27645  ex-xp  27647  ex-cnv  27648  ex-dm  27650  ex-rn  27651  ex-res  27652  ex-fv  27654  ex-1st  27655  ex-2nd  27656  hhph  28386  hlim0  28443  hsn0elch  28456  elch0  28462  hhssabloilem  28469  choc0  28536  shintcli  28539  shincli  28572  chincli  28670  h1deoi  28759  h1de2bi  28764  h1de2ctlem  28765  spansni  28767  df0op2  28962  ho01i  29038  nmop0h  29201  opsqrlem2  29351  opsqrlem4  29353  opsqrlem5  29354  hmopidmchi  29361  atoml2i  29593  xrge0iifhmeo  30330  rezh  30363  rrhre  30413  sxbrsigalem5  30698  carsgclctunlem2  30729  ballotth  30947  reprsuc  31041  reprlt  31045  reprgt  31047  circlemethnat  31067  circlevma  31068  bnj1015  31376  subfacp1lem3  31509  subfacp1lem5  31511  kur14lem7  31539  kur14lem9  31541  mrsubcv  31752  mrsubrn  31755  mvhf1  31801  msubvrs  31802  nofv  32153  sltres  32158  noextend  32162  noextendgt  32166  nolesgn2ores  32168  nosepnelem  32173  nosepdmlem  32176  nolt02o  32188  nosupno  32192  nosupbday  32194  nosupbnd1lem3  32199  nosupbnd1  32203  nosupbnd2lem1  32204  nosupbnd2  32205  onsucsuccmpi  32781  finxpreclem2  33562  poimirlem26  33767  poimirlem27  33768  poimir  33774  mbfresfi  33787  fdc  33871  rabren3dioph  37899  cllem0  38389  rclexi  38440  trclexi  38445  rtrclexi  38446  frege54cor1c  38727  dffrege76  38751  frege83  38758  frege97  38772  frege98  38773  dffrege99  38774  frege104  38779  frege109  38784  frege110  38785  frege131  38806  frege133  38808  clsk1indlem1  38861  clsk1independent  38862  rpex  40060  xrlexaddrp  40066  limsup10exlem  40502  limsup10ex  40503  wallispilem2  40780  stirlinglem14  40801  fourierdlem70  40890  fourierdlem83  40903  fourierdlem102  40922  fourierdlem103  40923  fourierdlem104  40924  fourierdlem114  40934  fouriersw  40945  sge0tsms  41094  omeunle  41230  0ome  41243  ovn0lem  41279  hoidmvlelem3  41311  ovnhoilem1  41315  vonicclem2  41398  mbfresmf  41448  smfpimcclem  41513
  Copyright terms: Public domain W3C validator