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  5296  funopdmsn  7154  caovmo  7658  pwen  9170  cnfcom2  9704  cnfcom3lem  9705  cnfcom3  9706  rankxplim3  9899  mappwen  10192  ackbij1lem5  10302  alephom  10671  inar1  10861  prlem934  11119  0idsr  11183  recexsrlem  11189  supsrlem  11197  opelreal  11216  elreal  11217  elreal2  11218  eqresr  11223  axmulass  11243  ax1ne0  11246  c0ex  11301  1ex  11304  2ex  12421  3ex  12426  elxr  13246  xnegex  13339  xaddval  13354  xmulval  13356  om2uzrdg  14100  hashxplem  14579  caucvgr  15844  rpnnen  16396  rexpen  16397  phimullem  16957  prmreclem6  17100  efgval  19932  cnfldfun  21693  cnfldfunALT  21694  psdmul  22488  psdmvr  22491  coe1mul2  22589  dscmet  24892  dscopn  24893  icopnfhmeo  25265  iccpnfhmeo  25267  xrhmeo  25268  bndth  25280  mbfimaopnlem  25977  mdegcl  26388  pige3ALT  26849  cxpval  26993  1cubr  27171  emcllem7  27330  basellem7  27415  prmorcht  27506  sqff1o  27510  ppiublem2  27531  lgsval  27629  lgsdir2lem3  27655  nofv  28015  ltsres  28020  noextend  28024  noextendgt  28028  nolesgn2ores  28030  nosepnelem  28037  nosepdmlem  28041  nolt02o  28053  nosupno  28061  nosupbnd1lem3  28068  nosupbnd1  28072  nosupbnd2lem1  28073  nosupbnd2  28074  0lt1s  28199  bday1  28201  cuteq0  28202  cuteq1  28204  mulsrid  28500  precsexlem9  28602  precsexlem11  28604  dfn0s2  28719  n0cut  28721  zsoring  28796  twocut  28810  expsval  28812  1reno  28884  axlowdimlem4  29524  axlowdimlem6  29526  upgrbi  29672  usgrexmpllem  29842  clwwlknon1sn  30692  uhgr3cyclex  30784  konigsberglem1  30854  konigsberglem2  30855  konigsberglem3  30856  ex-opab  31034  ex-eprel  31035  ex-id  31036  ex-xp  31038  ex-cnv  31039  ex-dm  31041  ex-rn  31042  ex-res  31043  ex-fv  31045  ex-1st  31046  ex-2nd  31047  hhph  31781  hlim0  31838  hsn0elch  31851  elch0  31857  hhssabloilem  31864  choc0  31929  shintcli  31932  shincli  31965  chincli  32063  h1deoi  32152  h1de2bi  32157  h1de2ctlem  32158  spansni  32160  df0op2  32355  ho01i  32431  nmop0h  32594  opsqrlem2  32744  opsqrlem4  32746  opsqrlem5  32747  hmopidmchi  32754  atoml2i  32986  s3clhash  33555  xrge0iifhmeo  34611  rezh  34644  rrhre  34696  sxbrsigalem5  34963  carsgclctunlem2  34994  ballotth  35213  reprsuc  35287  reprlt  35291  reprgt  35293  circlemethnat  35313  circlevma  35314  bnj1015  35635  subfacp1lem3  36016  subfacp1lem5  36018  kur14lem7  36046  kur14lem9  36048  mrsubcv  36344  mrsubrn  36347  mvhf1  36393  msubvrs  36394  onsucsuccmpi  37306  finxpreclem2  38389  poimirlem26  38640  poimirlem27  38641  poimir  38647  mbfresfi  38660  fdc  38755  rabren3dioph  43898  cllem0  44643  rclexi  44691  trclexi  44696  rtrclexi  44697  frege54cor1c  44991  dffrege76  45015  frege83  45022  frege97  45036  frege98  45037  dffrege99  45038  frege104  45043  frege109  45048  frege110  45049  frege131  45070  frege133  45072  clsk1independent  45122  imaexi  46310  xrlexaddrp  46440  limsup10exlem  46858  wallispilem2  47152  stirlinglem14  47173  fourierdlem70  47262  fourierdlem83  47275  fourierdlem102  47294  fourierdlem103  47295  fourierdlem104  47296  fourierdlem114  47306  fouriersw  47317  sge0tsms  47466  omeunle  47602  0ome  47615  ovn0lem  47651  hoidmvlelem3  47683  ovnhoilem1  47687  vonicclem2  47770  mbfresmf  47825  smfpimcclem  47893  lamberte  48014  nfermltl8rev  48916  nfermltlrev  48918  usgrexmpl1lem  49195  usgrexmpl2lem  49200  usgrexmpl2nb0  49205  usgrexmpl2nb3  49208  usgrexmpl2nb4  49209  usgrexmpl2nb5  49210  usgrexmpl2trifr  49211  veronesematbasd  51056  veroquadgsumlem  51059  veroquadmodzerod  51060  veroquadnolindfd  51061  veroquaddetzerod  51062