Theorem elexi 3513

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

Syntax hints:   ∈ wcel 2114  Vcvv 3494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-v 3496

This theorem is referenced by:  onunisuci  6304  funopdmsn  6912  caovmo  7385  1oex  8110  pwen  8690  cnfcom2  9165  cnfcom3lem  9166  cnfcom3  9167  rankxplim3  9310  mappwen  9538  ackbij1lem5  9646  alephom  10007  inar1  10197  prlem934  10455  0idsr  10519  recexsrlem  10525  supsrlem  10533  opelreal  10552  elreal  10553  elreal2  10554  eqresr  10559  axmulass  10579  ax1ne0  10582  c0ex  10635  1ex  10637  2ex  11715  3ex  11720  elxr  12512  xnegex  12602  xaddval  12617  xmulval  12619  om2uzrdg  13325  hashxplem  13795  caucvgr  15032  rpnnen  15580  rexpen  15581  phimullem  16116  prmreclem6  16257  efgval  18843  coe1mul2  20437  cnfldfun  20557  cnfldfunALT  20558  dscmet  23182  dscopn  23183  icopnfhmeo  23547  iccpnfhmeo  23549  xrhmeo  23550  bndth  23562  mbfimaopnlem  24256  mdegcl  24663  pige3ALT  25105  cxpval  25247  1cubr  25420  emcllem7  25579  basellem7  25664  prmorcht  25755  sqff1o  25759  ppiublem2  25779  lgsval  25877  lgsdir2lem3  25903  axlowdimlem4  26731  axlowdimlem6  26733  upgrbi  26878  usgrexmpllem  27042  clwwlknon1sn  27879  uhgr3cyclex  27961  konigsberglem1  28031  konigsberglem2  28032  konigsberglem3  28033  ex-opab  28211  ex-eprel  28212  ex-id  28213  ex-xp  28215  ex-cnv  28216  ex-dm  28218  ex-rn  28219  ex-res  28220  ex-fv  28222  ex-1st  28223  ex-2nd  28224  hhph  28955  hlim0  29012  hsn0elch  29025  elch0  29031  hhssabloilem  29038  choc0  29103  shintcli  29106  shincli  29139  chincli  29237  h1deoi  29326  h1de2bi  29331  h1de2ctlem  29332  spansni  29334  df0op2  29529  ho01i  29605  nmop0h  29768  opsqrlem2  29918  opsqrlem4  29920  opsqrlem5  29921  hmopidmchi  29928  atoml2i  30160  s3clhash  30624  xrge0iifhmeo  31179  rezh  31212  rrhre  31262  sxbrsigalem5  31546  carsgclctunlem2  31577  ballotth  31795  reprsuc  31886  reprlt  31890  reprgt  31892  circlemethnat  31912  circlevma  31913  bnj1015  32234  subfacp1lem3  32429  subfacp1lem5  32431  kur14lem7  32459  kur14lem9  32461  mrsubcv  32757  mrsubrn  32760  mvhf1  32806  msubvrs  32807  nofv  33164  sltres  33169  noextend  33173  noextendgt  33177  nolesgn2ores  33179  nosepnelem  33184  nosepdmlem  33187  nolt02o  33199  nosupno  33203  nosupbday  33205  nosupbnd1lem3  33210  nosupbnd1  33214  nosupbnd2lem1  33215  nosupbnd2  33216  onsucsuccmpi  33791  finxpreclem2  34674  poimirlem26  34933  poimirlem27  34934  poimir  34940  mbfresfi  34953  fdc  35035  rabren3dioph  39461  cllem0  39974  rclexi  40024  trclexi  40029  rtrclexi  40030  frege54cor1c  40310  dffrege76  40334  frege83  40341  frege97  40355  frege98  40356  dffrege99  40357  frege104  40362  frege109  40367  frege110  40368  frege131  40389  frege133  40391  clsk1independent  40445  rpex  41663  xrlexaddrp  41669  limsup10exlem  42102  wallispilem2  42400  stirlinglem14  42421  fourierdlem70  42510  fourierdlem83  42523  fourierdlem102  42542  fourierdlem103  42543  fourierdlem104  42544  fourierdlem114  42554  fouriersw  42565  sge0tsms  42711  omeunle  42847  0ome  42860  ovn0lem  42896  hoidmvlelem3  42928  ovnhoilem1  42932  vonicclem2  43015  mbfresmf  43065  smfpimcclem  43130  nfermltl8rev  43956  nfermltlrev  43958