Theorem elexi 3479

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459

This theorem is used by:  elpwi2  5308  funopdmsn  7153  caovmo  7657  pwen  9145  cnfcom2  9678  cnfcom3lem  9679  cnfcom3  9680  rankxplim3  9860  mappwen  10112  ackbij1lem5  10222  alephom  10587  inar1  10777  prlem934  11035  0idsr  11099  recexsrlem  11105  supsrlem  11113  opelreal  11132  elreal  11133  elreal2  11134  eqresr  11139  axmulass  11159  ax1ne0  11162  c0ex  11217  1ex  11220  2ex  12335  3ex  12340  elxr  13159  xnegex  13252  xaddval  13267  xmulval  13269  om2uzrdg  14012  hashxplem  14490  caucvgr  15753  rpnnen  16307  rexpen  16308  phimullem  16862  prmreclem6  17005  efgval  19833  cnfldfun  21588  cnfldfunALT  21589  psdmul  22381  psdmvr  22384  coe1mul2  22482  dscmet  24782  dscopn  24783  icopnfhmeo  25155  iccpnfhmeo  25157  xrhmeo  25158  bndth  25170  mbfimaopnlem  25867  mdegcl  26279  pige3ALT  26738  cxpval  26882  1cubr  27060  emcllem7  27219  basellem7  27304  prmorcht  27395  sqff1o  27399  ppiublem2  27420  lgsval  27518  lgsdir2lem3  27544  nofv  27874  ltsres  27879  noextend  27883  noextendgt  27887  nolesgn2ores  27889  nosepnelem  27896  nosepdmlem  27900  nolt02o  27912  nosupno  27920  nosupbnd1lem3  27927  nosupbnd1  27931  nosupbnd2lem1  27932  nosupbnd2  27933  0lt1s  28058  bday1  28060  cuteq0  28061  cuteq1  28063  mulsrid  28359  precsexlem9  28461  precsexlem11  28463  dfn0s2  28578  n0cut  28580  zsoring  28655  twocut  28669  expsval  28671  1reno  28743  axlowdimlem4  29352  axlowdimlem6  29354  upgrbi  29500  usgrexmpllem  29670  clwwlknon1sn  30520  uhgr3cyclex  30606  konigsberglem1  30676  konigsberglem2  30677  konigsberglem3  30678  ex-opab  30856  ex-eprel  30857  ex-id  30858  ex-xp  30860  ex-cnv  30861  ex-dm  30863  ex-rn  30864  ex-res  30865  ex-fv  30867  ex-1st  30868  ex-2nd  30869  hhph  31603  hlim0  31660  hsn0elch  31673  elch0  31679  hhssabloilem  31686  choc0  31751  shintcli  31754  shincli  31787  chincli  31885  h1deoi  31974  h1de2bi  31979  h1de2ctlem  31980  spansni  31982  df0op2  32177  ho01i  32253  nmop0h  32416  opsqrlem2  32566  opsqrlem4  32568  opsqrlem5  32569  hmopidmchi  32576  atoml2i  32808  s3clhash  33337  xrge0iifhmeo  34392  rezh  34425  rrhre  34477  sxbrsigalem5  34745  carsgclctunlem2  34776  ballotth  34995  reprsuc  35069  reprlt  35073  reprgt  35075  circlemethnat  35095  circlevma  35096  bnj1015  35417  subfacp1lem3  35713  subfacp1lem5  35715  kur14lem7  35743  kur14lem9  35745  mrsubcv  36041  mrsubrn  36044  mvhf1  36090  msubvrs  36091  onsucsuccmpi  37013  finxpreclem2  38095  poimirlem26  38356  poimirlem27  38357  poimir  38363  mbfresfi  38376  fdc  38456  rabren3dioph  43602  cllem0  44352  rclexi  44401  trclexi  44406  rtrclexi  44407  frege54cor1c  44701  dffrege76  44725  frege83  44732  frege97  44746  frege98  44747  dffrege99  44748  frege104  44753  frege109  44758  frege110  44759  frege131  44780  frege133  44782  clsk1independent  44832  imaexi  45997  xrlexaddrp  46128  limsup10exlem  46546  wallispilem2  46840  stirlinglem14  46861  fourierdlem70  46950  fourierdlem83  46963  fourierdlem102  46982  fourierdlem103  46983  fourierdlem104  46984  fourierdlem114  46994  fouriersw  47005  sge0tsms  47154  omeunle  47290  0ome  47303  ovn0lem  47339  hoidmvlelem3  47371  ovnhoilem1  47375  vonicclem2  47458  mbfresmf  47513  smfpimcclem  47581  lamberte  47685  nfermltl8rev  48567  nfermltlrev  48569  usgrexmpl1lem  48846  usgrexmpl2lem  48851  usgrexmpl2nb0  48856  usgrexmpl2nb3  48859  usgrexmpl2nb4  48860  usgrexmpl2nb5  48861  usgrexmpl2trifr  48862