Theorem elexi 3427

Description: If a class is a member of another class, then it is a set. Inference associated with elex 3426. (Contributed by NM, 11-Jun-1994.)

Hypothesis

Ref	Expression
elexi.1	⊢ 𝐴 ∈ 𝐵

Assertion

Ref	Expression
elexi	⊢ 𝐴 ∈ V

Proof of Theorem elexi

Step	Hyp	Ref	Expression
1		elexi.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		elex 3426	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ V

Syntax hints:   ∈ wcel 2110  Vcvv 3408

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410

This theorem is referenced by:  elpwi2  5239  onunisuci  6327  funopdmsn  6965  caovmo  7445  1oexOLD  8216  pwen  8819  cnfcom2  9317  cnfcom3lem  9318  cnfcom3  9319  rankxplim3  9497  mappwen  9726  ackbij1lem5  9838  alephom  10199  inar1  10389  prlem934  10647  0idsr  10711  recexsrlem  10717  supsrlem  10725  opelreal  10744  elreal  10745  elreal2  10746  eqresr  10751  axmulass  10771  ax1ne0  10774  c0ex  10827  1ex  10829  2ex  11907  3ex  11912  elxr  12708  xnegex  12798  xaddval  12813  xmulval  12815  om2uzrdg  13529  hashxplem  14000  caucvgr  15239  rpnnen  15788  rexpen  15789  phimullem  16332  prmreclem6  16474  efgval  19107  cnfldfun  20375  cnfldfunALT  20376  coe1mul2  21190  dscmet  23470  dscopn  23471  icopnfhmeo  23840  iccpnfhmeo  23842  xrhmeo  23843  bndth  23855  mbfimaopnlem  24552  mdegcl  24967  pige3ALT  25409  cxpval  25552  1cubr  25725  emcllem7  25884  basellem7  25969  prmorcht  26060  sqff1o  26064  ppiublem2  26084  lgsval  26182  lgsdir2lem3  26208  axlowdimlem4  27036  axlowdimlem6  27038  upgrbi  27184  usgrexmpllem  27348  clwwlknon1sn  28183  uhgr3cyclex  28265  konigsberglem1  28335  konigsberglem2  28336  konigsberglem3  28337  ex-opab  28515  ex-eprel  28516  ex-id  28517  ex-xp  28519  ex-cnv  28520  ex-dm  28522  ex-rn  28523  ex-res  28524  ex-fv  28526  ex-1st  28527  ex-2nd  28528  hhph  29259  hlim0  29316  hsn0elch  29329  elch0  29335  hhssabloilem  29342  choc0  29407  shintcli  29410  shincli  29443  chincli  29541  h1deoi  29630  h1de2bi  29635  h1de2ctlem  29636  spansni  29638  df0op2  29833  ho01i  29909  nmop0h  30072  opsqrlem2  30222  opsqrlem4  30224  opsqrlem5  30225  hmopidmchi  30232  atoml2i  30464  s3clhash  30942  xrge0iifhmeo  31600  rezh  31633  rrhre  31683  sxbrsigalem5  31967  carsgclctunlem2  31998  ballotth  32216  reprsuc  32307  reprlt  32311  reprgt  32313  circlemethnat  32333  circlevma  32334  bnj1015  32655  subfacp1lem3  32857  subfacp1lem5  32859  kur14lem7  32887  kur14lem9  32889  mrsubcv  33185  mrsubrn  33188  mvhf1  33234  msubvrs  33235  nofv  33597  sltres  33602  noextend  33606  noextendgt  33610  nolesgn2ores  33612  nosepnelem  33619  nosepdmlem  33623  nolt02o  33635  nosupno  33643  nosupbnd1lem3  33650  nosupbnd1  33654  nosupbnd2lem1  33655  nosupbnd2  33656  0slt1s  33760  bday1s  33762  onsucsuccmpi  34369  finxpreclem2  35298  poimirlem26  35540  poimirlem27  35541  poimir  35547  mbfresfi  35560  fdc  35640  rabren3dioph  40340  cllem0  40849  rclexi  40899  trclexi  40904  rtrclexi  40905  frege54cor1c  41200  dffrege76  41224  frege83  41231  frege97  41245  frege98  41246  dffrege99  41247  frege104  41252  frege109  41257  frege110  41258  frege131  41279  frege133  41281  clsk1independent  41333  rpex  42558  xrlexaddrp  42564  limsup10exlem  42988  wallispilem2  43282  stirlinglem14  43303  fourierdlem70  43392  fourierdlem83  43405  fourierdlem102  43424  fourierdlem103  43425  fourierdlem104  43426  fourierdlem114  43436  fouriersw  43447  sge0tsms  43593  omeunle  43729  0ome  43742  ovn0lem  43778  hoidmvlelem3  43810  ovnhoilem1  43814  vonicclem2  43897  mbfresmf  43947  smfpimcclem  44012  nfermltl8rev  44867  nfermltlrev  44869