Theorem elexi 3473

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453

This theorem is used by:  elpwi2  5297  funopdmsn  7154  caovmo  7658  pwen  9169  cnfcom2  9703  cnfcom3lem  9704  cnfcom3  9705  rankxplim3  9898  mappwen  10191  ackbij1lem5  10301  alephom  10670  inar1  10860  prlem934  11118  0idsr  11182  recexsrlem  11188  supsrlem  11196  opelreal  11215  elreal  11216  elreal2  11217  eqresr  11222  axmulass  11242  ax1ne0  11245  c0ex  11300  1ex  11303  2ex  12420  3ex  12425  elxr  13245  xnegex  13338  xaddval  13353  xmulval  13355  om2uzrdg  14099  hashxplem  14578  caucvgr  15843  rpnnen  16395  rexpen  16396  phimullem  16956  prmreclem6  17099  efgval  19931  cnfldfun  21692  cnfldfunALT  21693  psdmul  22487  psdmvr  22490  coe1mul2  22588  dscmet  24891  dscopn  24892  icopnfhmeo  25264  iccpnfhmeo  25266  xrhmeo  25267  bndth  25279  mbfimaopnlem  25976  mdegcl  26387  pige3ALT  26848  cxpval  26992  1cubr  27170  emcllem7  27329  basellem7  27414  prmorcht  27505  sqff1o  27509  ppiublem2  27530  lgsval  27628  lgsdir2lem3  27654  nofv  28014  ltsres  28019  noextend  28023  noextendgt  28027  nolesgn2ores  28029  nosepnelem  28036  nosepdmlem  28040  nolt02o  28052  nosupno  28060  nosupbnd1lem3  28067  nosupbnd1  28071  nosupbnd2lem1  28072  nosupbnd2  28073  0lt1s  28198  bday1  28200  cuteq0  28201  cuteq1  28203  mulsrid  28499  precsexlem9  28601  precsexlem11  28603  dfn0s2  28718  n0cut  28720  zsoring  28795  twocut  28809  expsval  28811  1reno  28883  axlowdimlem4  29523  axlowdimlem6  29525  upgrbi  29671  usgrexmpllem  29841  clwwlknon1sn  30691  uhgr3cyclex  30783  konigsberglem1  30853  konigsberglem2  30854  konigsberglem3  30855  ex-opab  31033  ex-eprel  31034  ex-id  31035  ex-xp  31037  ex-cnv  31038  ex-dm  31040  ex-rn  31041  ex-res  31042  ex-fv  31044  ex-1st  31045  ex-2nd  31046  hhph  31780  hlim0  31837  hsn0elch  31850  elch0  31856  hhssabloilem  31863  choc0  31928  shintcli  31931  shincli  31964  chincli  32062  h1deoi  32151  h1de2bi  32156  h1de2ctlem  32157  spansni  32159  df0op2  32354  ho01i  32430  nmop0h  32593  opsqrlem2  32743  opsqrlem4  32745  opsqrlem5  32746  hmopidmchi  32753  atoml2i  32985  s3clhash  33512  xrge0iifhmeo  34568  rezh  34601  rrhre  34653  sxbrsigalem5  34920  carsgclctunlem2  34951  ballotth  35170  reprsuc  35244  reprlt  35248  reprgt  35250  circlemethnat  35270  circlevma  35271  bnj1015  35592  subfacp1lem3  35947  subfacp1lem5  35949  kur14lem7  35977  kur14lem9  35979  mrsubcv  36275  mrsubrn  36278  mvhf1  36324  msubvrs  36325  onsucsuccmpi  37231  finxpreclem2  38313  poimirlem26  38564  poimirlem27  38565  poimir  38571  mbfresfi  38584  fdc  38679  rabren3dioph  43821  cllem0  44566  rclexi  44614  trclexi  44619  rtrclexi  44620  frege54cor1c  44914  dffrege76  44938  frege83  44945  frege97  44959  frege98  44960  dffrege99  44961  frege104  44966  frege109  44971  frege110  44972  frege131  44993  frege133  44995  clsk1independent  45045  imaexi  46233  xrlexaddrp  46363  limsup10exlem  46781  wallispilem2  47075  stirlinglem14  47096  fourierdlem70  47185  fourierdlem83  47198  fourierdlem102  47217  fourierdlem103  47218  fourierdlem104  47219  fourierdlem114  47229  fouriersw  47240  sge0tsms  47389  omeunle  47525  0ome  47538  ovn0lem  47574  hoidmvlelem3  47606  ovnhoilem1  47610  vonicclem2  47693  mbfresmf  47748  smfpimcclem  47816  lamberte  47937  nfermltl8rev  48839  nfermltlrev  48841  usgrexmpl1lem  49118  usgrexmpl2lem  49123  usgrexmpl2nb0  49128  usgrexmpl2nb3  49131  usgrexmpl2nb4  49132  usgrexmpl2nb5  49133  usgrexmpl2trifr  49134  veronesematbasd  50979  veroquadgsumlem  50982  veroquadmodzerod  50983  veroquadnolindfd  50984  veroquaddetzerod  50985