Theorem elexi 3441

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

Syntax hints:   ∈ wcel 2108  Vcvv 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424

This theorem is referenced by:  elpwi2  5265  onunisuci  6365  funopdmsn  7004  caovmo  7487  1oexOLD  8281  pwen  8886  cnfcom2  9390  cnfcom3lem  9391  cnfcom3  9392  rankxplim3  9570  mappwen  9799  ackbij1lem5  9911  alephom  10272  inar1  10462  prlem934  10720  0idsr  10784  recexsrlem  10790  supsrlem  10798  opelreal  10817  elreal  10818  elreal2  10819  eqresr  10824  axmulass  10844  ax1ne0  10847  c0ex  10900  1ex  10902  2ex  11980  3ex  11985  elxr  12781  xnegex  12871  xaddval  12886  xmulval  12888  om2uzrdg  13604  hashxplem  14076  caucvgr  15315  rpnnen  15864  rexpen  15865  phimullem  16408  prmreclem6  16550  efgval  19238  cnfldfun  20522  cnfldfunALT  20523  coe1mul2  21350  dscmet  23634  dscopn  23635  icopnfhmeo  24012  iccpnfhmeo  24014  xrhmeo  24015  bndth  24027  mbfimaopnlem  24724  mdegcl  25139  pige3ALT  25581  cxpval  25724  1cubr  25897  emcllem7  26056  basellem7  26141  prmorcht  26232  sqff1o  26236  ppiublem2  26256  lgsval  26354  lgsdir2lem3  26380  axlowdimlem4  27216  axlowdimlem6  27218  upgrbi  27366  usgrexmpllem  27530  clwwlknon1sn  28365  uhgr3cyclex  28447  konigsberglem1  28517  konigsberglem2  28518  konigsberglem3  28519  ex-opab  28697  ex-eprel  28698  ex-id  28699  ex-xp  28701  ex-cnv  28702  ex-dm  28704  ex-rn  28705  ex-res  28706  ex-fv  28708  ex-1st  28709  ex-2nd  28710  hhph  29441  hlim0  29498  hsn0elch  29511  elch0  29517  hhssabloilem  29524  choc0  29589  shintcli  29592  shincli  29625  chincli  29723  h1deoi  29812  h1de2bi  29817  h1de2ctlem  29818  spansni  29820  df0op2  30015  ho01i  30091  nmop0h  30254  opsqrlem2  30404  opsqrlem4  30406  opsqrlem5  30407  hmopidmchi  30414  atoml2i  30646  s3clhash  31124  xrge0iifhmeo  31788  rezh  31821  rrhre  31871  sxbrsigalem5  32155  carsgclctunlem2  32186  ballotth  32404  reprsuc  32495  reprlt  32499  reprgt  32501  circlemethnat  32521  circlevma  32522  bnj1015  32842  subfacp1lem3  33044  subfacp1lem5  33046  kur14lem7  33074  kur14lem9  33076  mrsubcv  33372  mrsubrn  33375  mvhf1  33421  msubvrs  33422  nofv  33787  sltres  33792  noextend  33796  noextendgt  33800  nolesgn2ores  33802  nosepnelem  33809  nosepdmlem  33813  nolt02o  33825  nosupno  33833  nosupbnd1lem3  33840  nosupbnd1  33844  nosupbnd2lem1  33845  nosupbnd2  33846  0slt1s  33950  bday1s  33952  onsucsuccmpi  34559  finxpreclem2  35488  poimirlem26  35730  poimirlem27  35731  poimir  35737  mbfresfi  35750  fdc  35830  rabren3dioph  40553  cllem0  41062  rclexi  41112  trclexi  41117  rtrclexi  41118  frege54cor1c  41412  dffrege76  41436  frege83  41443  frege97  41457  frege98  41458  dffrege99  41459  frege104  41464  frege109  41469  frege110  41470  frege131  41491  frege133  41493  clsk1independent  41545  rpex  42775  xrlexaddrp  42781  limsup10exlem  43203  wallispilem2  43497  stirlinglem14  43518  fourierdlem70  43607  fourierdlem83  43620  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem114  43651  fouriersw  43662  sge0tsms  43808  omeunle  43944  0ome  43957  ovn0lem  43993  hoidmvlelem3  44025  ovnhoilem1  44029  vonicclem2  44112  mbfresmf  44162  smfpimcclem  44227  nfermltl8rev  45082  nfermltlrev  45084