Theorem elexi 3472

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  elpwi2  5297  funopdmsn  7159  caovmo  7662  pwen  9177  cnfcom2  9710  cnfcom3lem  9711  cnfcom3  9712  rankxplim3  9905  mappwen  10198  ackbij1lem5  10308  alephom  10677  inar1  10867  prlem934  11125  0idsr  11189  recexsrlem  11195  supsrlem  11203  opelreal  11222  elreal  11223  elreal2  11224  eqresr  11229  axmulass  11249  ax1ne0  11252  c0ex  11307  1ex  11310  2ex  12427  3ex  12432  elxr  13252  xnegex  13345  xaddval  13360  xmulval  13362  om2uzrdg  14106  hashxplem  14585  caucvgr  15852  rpnnen  16404  rexpen  16405  phimullem  16965  prmreclem6  17108  efgval  19940  cnfldfun  21701  cnfldfunALT  21702  psdmul  22496  psdmvr  22499  coe1mul2  22597  dscmet  24900  dscopn  24901  icopnfhmeo  25273  iccpnfhmeo  25275  xrhmeo  25276  bndth  25288  mbfimaopnlem  25985  mdegcl  26396  pige3ALT  26857  cxpval  27001  1cubr  27179  emcllem7  27338  basellem7  27423  prmorcht  27514  sqff1o  27518  ppiublem2  27539  lgsval  27637  lgsdir2lem3  27663  nofv  28023  ltsres  28028  noextend  28032  noextendgt  28036  nolesgn2ores  28038  nosepnelem  28045  nosepdmlem  28049  nolt02o  28061  nosupno  28069  nosupbnd1lem3  28076  nosupbnd1  28080  nosupbnd2lem1  28081  nosupbnd2  28082  0lt1s  28207  bday1  28209  cuteq0  28210  cuteq1  28212  mulsrid  28508  precsexlem9  28610  precsexlem11  28612  dfn0s2  28727  n0cut  28729  zsoring  28804  twocut  28818  expsval  28820  1reno  28892  axlowdimlem4  29532  axlowdimlem6  29534  upgrbi  29680  usgrexmpllem  29850  clwwlknon1sn  30700  uhgr3cyclex  30792  konigsberglem1  30862  konigsberglem2  30863  konigsberglem3  30864  ex-opab  31042  ex-eprel  31043  ex-id  31044  ex-xp  31046  ex-cnv  31047  ex-dm  31049  ex-rn  31050  ex-res  31051  ex-fv  31053  ex-1st  31054  ex-2nd  31055  hhph  31789  hlim0  31846  hsn0elch  31859  elch0  31865  hhssabloilem  31872  choc0  31937  shintcli  31940  shincli  31973  chincli  32071  h1deoi  32160  h1de2bi  32165  h1de2ctlem  32166  spansni  32168  df0op2  32363  ho01i  32439  nmop0h  32602  opsqrlem2  32752  opsqrlem4  32754  opsqrlem5  32755  hmopidmchi  32762  atoml2i  32994  s3clhash  33562  xrge0iifhmeo  34618  rezh  34651  rrhre  34703  sxbrsigalem5  34970  carsgclctunlem2  35001  ballotth  35220  reprsuc  35294  reprlt  35298  reprgt  35300  circlemethnat  35320  circlevma  35321  bnj1015  35642  jltalephlem  35976  subfacp1lem3  36065  subfacp1lem5  36067  kur14lem7  36095  kur14lem9  36097  mrsubcv  36393  mrsubrn  36396  mvhf1  36442  msubvrs  36443  onsucsuccmpi  37355  finxpreclem2  38450  poimirlem26  38701  poimirlem27  38702  poimir  38708  mbfresfi  38721  fdc  38816  rabren3dioph  43959  cllem0  44704  rclexi  44752  trclexi  44757  rtrclexi  44758  frege54cor1c  45052  dffrege76  45076  frege83  45083  frege97  45097  frege98  45098  dffrege99  45099  frege104  45104  frege109  45109  frege110  45110  frege131  45131  frege133  45133  clsk1independent  45183  imaexi  46370  xrlexaddrp  46500  limsup10exlem  46918  wallispilem2  47212  stirlinglem14  47233  fourierdlem70  47322  fourierdlem83  47335  fourierdlem102  47354  fourierdlem103  47355  fourierdlem104  47356  fourierdlem114  47366  fouriersw  47377  sge0tsms  47526  omeunle  47662  0ome  47675  ovn0lem  47711  hoidmvlelem3  47743  ovnhoilem1  47747  vonicclem2  47830  mbfresmf  47885  smfpimcclem  47953  lamberte  48074  nfermltl8rev  48976  nfermltlrev  48978  usgrexmpl1lem  49255  usgrexmpl2lem  49260  usgrexmpl2nb0  49265  usgrexmpl2nb3  49268  usgrexmpl2nb4  49269  usgrexmpl2nb5  49270  usgrexmpl2trifr  49271  veronesematbasd  51191  veroquadgsumlem  51194  veroquadmodzerod  51195  veroquadnolindfd  51196  veroquaddetzerod  51197