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

Theorem elexi 3467
Description: If a class is a member of another class, then it is a set. Inference associated with elex 3466. (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 3466 . 2 (𝐴𝐵𝐴 ∈ V)
31, 2ax-mp 5 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3448
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450
This theorem is referenced by:  elpwi2  5308  funopdmsn  7101  caovmo  7596  1oexOLD  8437  pwen  9101  cnfcom2  9645  cnfcom3lem  9646  cnfcom3  9647  rankxplim3  9824  mappwen  10055  ackbij1lem5  10167  alephom  10528  inar1  10718  prlem934  10976  0idsr  11040  recexsrlem  11046  supsrlem  11054  opelreal  11073  elreal  11074  elreal2  11075  eqresr  11080  axmulass  11100  ax1ne0  11103  c0ex  11156  1ex  11158  2ex  12237  3ex  12242  elxr  13044  xnegex  13134  xaddval  13149  xmulval  13151  om2uzrdg  13868  hashxplem  14340  caucvgr  15567  rpnnen  16116  rexpen  16117  phimullem  16658  prmreclem6  16800  efgval  19506  cnfldfun  20824  cnfldfunALT  20825  cnfldfunALTOLD  20826  coe1mul2  21656  dscmet  23944  dscopn  23945  icopnfhmeo  24322  iccpnfhmeo  24324  xrhmeo  24325  bndth  24337  mbfimaopnlem  25035  mdegcl  25450  pige3ALT  25892  cxpval  26035  1cubr  26208  emcllem7  26367  basellem7  26452  prmorcht  26543  sqff1o  26547  ppiublem2  26567  lgsval  26665  lgsdir2lem3  26691  nofv  27021  sltres  27026  noextend  27030  noextendgt  27034  nolesgn2ores  27036  nosepnelem  27043  nosepdmlem  27047  nolt02o  27059  nosupno  27067  nosupbnd1lem3  27074  nosupbnd1  27078  nosupbnd2lem1  27079  nosupbnd2  27080  0slt1s  27190  bday1s  27192  cuteq0  27193  mulsrid  27399  mulslid  27400  axlowdimlem4  27936  axlowdimlem6  27938  upgrbi  28086  usgrexmpllem  28250  clwwlknon1sn  29086  uhgr3cyclex  29168  konigsberglem1  29238  konigsberglem2  29239  konigsberglem3  29240  ex-opab  29418  ex-eprel  29419  ex-id  29420  ex-xp  29422  ex-cnv  29423  ex-dm  29425  ex-rn  29426  ex-res  29427  ex-fv  29429  ex-1st  29430  ex-2nd  29431  hhph  30162  hlim0  30219  hsn0elch  30232  elch0  30238  hhssabloilem  30245  choc0  30310  shintcli  30313  shincli  30346  chincli  30444  h1deoi  30533  h1de2bi  30538  h1de2ctlem  30539  spansni  30541  df0op2  30736  ho01i  30812  nmop0h  30975  opsqrlem2  31125  opsqrlem4  31127  opsqrlem5  31128  hmopidmchi  31135  atoml2i  31367  s3clhash  31846  xrge0iifhmeo  32557  rezh  32592  rrhre  32642  sxbrsigalem5  32928  carsgclctunlem2  32959  ballotth  33177  reprsuc  33268  reprlt  33272  reprgt  33274  circlemethnat  33294  circlevma  33295  bnj1015  33614  subfacp1lem3  33816  subfacp1lem5  33818  kur14lem7  33846  kur14lem9  33848  mrsubcv  34144  mrsubrn  34147  mvhf1  34193  msubvrs  34194  onsucsuccmpi  34944  finxpreclem2  35890  poimirlem26  36133  poimirlem27  36134  poimir  36140  mbfresfi  36153  fdc  36233  rabren3dioph  41167  cllem0  41912  rclexi  41961  trclexi  41966  rtrclexi  41967  frege54cor1c  42261  dffrege76  42285  frege83  42292  frege97  42306  frege98  42307  dffrege99  42308  frege104  42313  frege109  42318  frege110  42319  frege131  42340  frege133  42342  clsk1independent  42392  rpex  43654  xrlexaddrp  43660  limsup10exlem  44087  wallispilem2  44381  stirlinglem14  44402  fourierdlem70  44491  fourierdlem83  44504  fourierdlem102  44523  fourierdlem103  44524  fourierdlem104  44525  fourierdlem114  44535  fouriersw  44546  sge0tsms  44695  omeunle  44831  0ome  44844  ovn0lem  44880  hoidmvlelem3  44912  ovnhoilem1  44916  vonicclem2  44999  mbfresmf  45054  smfpimcclem  45122  nfermltl8rev  46008  nfermltlrev  46010
  Copyright terms: Public domain W3C validator