Theorem elexi 3477

Description: If a class is a member of another class, then it is a set. Inference associated with elex 3476. (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 3476	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ V

Syntax hints:   ∈ wcel 2143  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457

This theorem is referenced by:  elpwi2  5306  funopdmsn  7147  caovmo  7647  pwen  9134  cnfcom2  9667  cnfcom3lem  9668  cnfcom3  9669  rankxplim3  9849  mappwen  10092  ackbij1lem5  10202  alephom  10565  inar1  10755  prlem934  11013  0idsr  11077  recexsrlem  11083  supsrlem  11091  opelreal  11110  elreal  11111  elreal2  11112  eqresr  11117  axmulass  11137  ax1ne0  11140  c0ex  11195  1ex  11198  2ex  12313  3ex  12318  elxr  13136  xnegex  13229  xaddval  13244  xmulval  13246  om2uzrdg  13988  hashxplem  14466  caucvgr  15723  rpnnen  16278  rexpen  16279  phimullem  16833  prmreclem6  16976  efgval  19782  cnfldfun  21536  cnfldfunALT  21537  psdmul  22329  psdmvr  22332  coe1mul2  22430  dscmet  24729  dscopn  24730  icopnfhmeo  25102  iccpnfhmeo  25104  xrhmeo  25105  bndth  25117  mbfimaopnlem  25814  mdegcl  26226  pige3ALT  26685  cxpval  26829  1cubr  27007  emcllem7  27166  basellem7  27251  prmorcht  27342  sqff1o  27346  ppiublem2  27367  lgsval  27465  lgsdir2lem3  27491  nofv  27821  ltsres  27826  noextend  27830  noextendgt  27834  nolesgn2ores  27836  nosepnelem  27843  nosepdmlem  27847  nolt02o  27859  nosupno  27867  nosupbnd1lem3  27874  nosupbnd1  27878  nosupbnd2lem1  27879  nosupbnd2  27880  0lt1s  28005  bday1  28007  cuteq0  28008  cuteq1  28010  mulsrid  28306  precsexlem9  28408  precsexlem11  28410  dfn0s2  28525  n0cut  28527  zsoring  28602  twocut  28616  expsval  28618  1reno  28690  axlowdimlem4  29295  axlowdimlem6  29297  upgrbi  29443  usgrexmpllem  29610  clwwlknon1sn  30451  uhgr3cyclex  30533  konigsberglem1  30603  konigsberglem2  30604  konigsberglem3  30605  ex-opab  30783  ex-eprel  30784  ex-id  30785  ex-xp  30787  ex-cnv  30788  ex-dm  30790  ex-rn  30791  ex-res  30792  ex-fv  30794  ex-1st  30795  ex-2nd  30796  hhph  31530  hlim0  31587  hsn0elch  31600  elch0  31606  hhssabloilem  31613  choc0  31678  shintcli  31681  shincli  31714  chincli  31812  h1deoi  31901  h1de2bi  31906  h1de2ctlem  31907  spansni  31909  df0op2  32104  ho01i  32180  nmop0h  32343  opsqrlem2  32493  opsqrlem4  32495  opsqrlem5  32496  hmopidmchi  32503  atoml2i  32735  s3clhash  33268  xrge0iifhmeo  34326  rezh  34359  rrhre  34411  sxbrsigalem5  34678  carsgclctunlem2  34709  ballotth  34928  reprsuc  35002  reprlt  35006  reprgt  35008  circlemethnat  35028  circlevma  35029  bnj1015  35350  subfacp1lem3  35674  subfacp1lem5  35676  kur14lem7  35704  kur14lem9  35706  mrsubcv  36002  mrsubrn  36005  mvhf1  36051  msubvrs  36052  onsucsuccmpi  36974  finxpreclem2  38056  poimirlem26  38317  poimirlem27  38318  poimir  38324  mbfresfi  38337  fdc  38416  rabren3dioph  43562  cllem0  44312  rclexi  44361  trclexi  44366  rtrclexi  44367  frege54cor1c  44661  dffrege76  44685  frege83  44692  frege97  44706  frege98  44707  dffrege99  44708  frege104  44713  frege109  44718  frege110  44719  frege131  44740  frege133  44742  clsk1independent  44792  imaexi  45957  xrlexaddrp  46088  limsup10exlem  46506  wallispilem2  46800  stirlinglem14  46821  fourierdlem70  46910  fourierdlem83  46923  fourierdlem102  46942  fourierdlem103  46943  fourierdlem104  46944  fourierdlem114  46954  fouriersw  46965  sge0tsms  47114  omeunle  47250  0ome  47263  ovn0lem  47299  hoidmvlelem3  47331  ovnhoilem1  47335  vonicclem2  47418  mbfresmf  47473  smfpimcclem  47541  lamberte  47645  nfermltl8rev  48527  nfermltlrev  48529  usgrexmpl1lem  48806  usgrexmpl2lem  48811  usgrexmpl2nb0  48816  usgrexmpl2nb3  48819  usgrexmpl2nb4  48820  usgrexmpl2nb5  48821  usgrexmpl2trifr  48822