Theorem elex 3461

Description: If a class is a member of another class, then it is a set. Theorem 6.12 of [Quine] p. 44. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Proof shortened by Wolf Lammen, 28-May-2025.)

Assertion

Ref	Expression
elex	⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)

Proof of Theorem elex

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elissetv 2817	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
2		isset 3454	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
3	1, 2	sylibr 234	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1541  ∃wex 1780   ∈ wcel 2113  Vcvv 3440

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442

This theorem is referenced by:  elexi  3463  elexd  3464  prcnel  3466  spcimgfi1OLD  3505  vtoclgf  3525  vtocl2gf  3527  vtocl3gf  3528  vtocl2g  3529  vtocl3g  3530  spcgv  3550  spc3egv  3557  elab4g  3638  elrabf  3643  elrab  3646  elrab2w  3650  class2seteq  3662  mob  3675  sbcex  3750  sbcel1v  3806  sbcabel  3828  csbiebt  3878  eldif  3911  elin  3917  ssv  3958  elun  4105  csbnestgfw  4374  sbcco3gw  4377  csbnestgf  4379  sbcco3g  4382  csbco3g  4383  csbvarg  4386  sbccsb2  4389  elpwb  4562  pwidb  4575  elpr2g  4606  snidb  4618  ifpr  4650  snssg  4740  eldifvsn  4753  preqsnd  4815  elpreqpr  4823  dfopg  4827  eluni  4866  eliun  4950  csbexg  5255  nvel  5261  axpweq  5296  reusv2lem4  5346  elopab  5475  epelg  5525  opelvvg  5665  opeliunxp2  5787  opelres  5944  imasng  6043  elimasni  6050  iniseg  6056  inisegn0  6057  dmmptg  6200  elon2  6328  ordsssuc2  6410  iota2  6481  fnmptf  6628  fnmpt  6632  fvelimab  6906  mpteqb  6960  fvmptt  6961  fvmptf  6962  fvopab5  6974  fvopab6  6975  fprg  7100  eloprabga  7467  ovmpos  7506  ov2gf  7507  ovmpox  7511  ovmpoga  7512  ovmpt3rab1  7616  brrpssg  7670  sorpssi  7674  unexgOLD  7694  elpwun  7714  ordeleqon  7727  onintrab  7741  sucexg  7750  sucexeloni  7754  ordsucelsuc  7764  onzsl  7788  dmfexALT  7850  elxp5  7865  fabexg  7880  f1oabexg  7884  offval3  7926  releldm2  7987  fnmpo  8013  mpoexg  8020  bropfvvvv  8034  fsplitfpar  8060  suppval  8104  opeliunxp2f  8152  brtpos2  8174  undefval  8218  tfr2b  8327  tz7.49  8376  oeordi  8515  relelec  8682  ecdmn0  8687  mapvalg  8773  pmvalg  8774  elpmg  8780  elixp2  8839  mptelixpg  8873  elixpsn  8875  2pwuninel  9060  ordfin  9140  rex2dom  9153  fival  9315  elfi2  9317  dffi2  9326  elfiun  9333  wemapso2lem  9457  harval  9465  brwdom  9472  fowdom  9476  brwdom2  9478  brwdom3  9487  en2lp  9515  cantnfsuc  9579  rankvalb  9709  rankwflem  9727  rankr1g  9744  r1pwALT  9758  r1rankid  9771  djulcl  9822  djurcl  9823  inlresf  9826  inrresf  9828  djuss  9832  1stinl  9839  2ndinl  9840  1stinr  9841  2ndinr  9842  cardval3  9864  dfac8alem  9939  isacn  9954  numacn  9959  acndom  9961  cardinfima  10007  unialeph  10011  ackbij1lem5  10133  cflm  10160  isf32lem2  10264  isfin1-2  10295  itunifval  10326  numth3  10380  ttukeylem1  10419  cardidg  10458  ondomon  10473  elwina  10597  elina  10598  wuncval  10653  tskmval  10750  eltskm  10754  recmulnq  10875  elnp  10898  elnpi  10899  npomex  10907  elfzp12  13519  seqp1  13939  hashinf  14258  hashxnn0  14262  hashnn0pnf  14265  hashxrcl  14280  prsshashgt1  14333  hashmap  14358  lsw  14487  ccatfval  14496  ccats1alpha  14543  swrdval  14567  pfxval  14597  splval  14674  splcl  14675  revval  14683  reps  14693  s3sndisj  14890  s3iunsndisj  14891  trclfv  14923  relexp0g  14945  relexpsucnnr  14948  relexp1g  14949  limsupcl  15396  limsupval  15397  clim  15417  rlim  15418  hashbcval  16930  isstruct2  17076  setsvalg  17093  setsfun0  17099  setscom  17107  strfvnd  17112  setsid  17134  ressval  17160  ressinbas  17172  restval  17346  pwsval  17406  xpsfrnel2  17485  ismre  17509  oppcval  17636  oppccatf  17651  brssc  17738  rescval  17751  issubc  17759  isfunc  17788  homadm  17964  homacd  17965  uncfval  18157  pltfval  18252  lubfval  18271  glbfval  18284  joinfval  18294  meetfval  18308  p0val  18348  p1val  18349  oduclatb  18430  ipoval  18453  pws0g  18698  frmdval  18776  vrmdfval  18781  efmnd  18795  efmnd2hash  18819  eqgfval  19105  gaid  19228  cntzfval  19249  elsymgbas  19303  symg2hash  19321  pmtrfval  19379  symggen  19399  gexval  19507  lsmfval  19567  pj1fval  19623  frgpval  19687  vrgpfval  19695  dmdprd  19929  dprdw  19941  pws1  20260  pwsmgp  20262  dvdsr  20298  isrngim  20381  rgspnval  20545  rnghmsscmap  20563  rhmsscmap  20592  lssset  20884  lspfval  20924  islbs  21028  sraval  21127  zlmval  21470  psgnevpmb  21542  ocvfval  21621  cssval  21637  thlval  21650  dsmmval  21689  dsmmbase  21690  frlmval  21703  uvcfval  21739  islinds  21764  ltbval  21998  evlsval  22041  coe1fval  22146  evls1fval  22263  matval  22355  oftpos  22396  dmatval  22436  scmatval  22448  smadiadetglem2  22616  cpmat  22653  mat2pmatfval  22667  cpm2mfval  22693  decpmatval0  22708  pm2mpval  22739  chpmatfval  22774  basdif0  22897  tgval  22899  eltg  22901  eltg2  22902  neipeltop  23073  ordtval  23133  islocfin  23461  txval  23508  qtopval  23639  isfbas  23773  isfildlem  23801  fmval  23887  fmf  23889  isfcls  23953  alexsubb  23990  tsmsfbas  24072  ustval  24147  elutop  24177  isusp  24205  ispsmet  24248  ismet  24267  isxmet  24268  blfvalps  24327  metustel  24494  tngval  24583  elpi1  25001  rrxval  25343  q1peqb  26117  ig1pval  26137  taylfval  26322  ulmval  26345  elno  27613  elnoOLD  27614  nosupno  27671  noetalem2  27710  nulslts  27771  oldlim  27883  negsval  28021  elz12s  28468  iscgrg  28584  isismt  28606  legval  28656  ishlg  28674  ishpg  28831  iscgra  28881  isinag  28910  isleag  28919  iseqlg  28939  ttgval  28947  xmstrkgc  28958  cplgr2vpr  29506  vtxdgfval  29541  ewlksfval  29675  wksfval  29683  iswlkg  29687  wwlksnon  29924  wspthsnon  29925  avril1  30538  ispligb  30552  gidval  30587  isvcOLD  30654  0vfval  30681  elunop  31947  rabexgfGS  32574  disjdifprg  32650  disjdifprg2  32651  abfmpunirn  32730  rabfmpunirn  32731  hashgt1  32888  indv  32931  mntoval  33064  tocycval  33190  evpmval  33227  altgnsg  33231  sgnsv  33242  inftmrel  33262  isinftm  33263  resvval  33410  ellpi  33454  idlsrgval  33584  rprmval  33597  dimval  33757  dimvalfi  33758  smatfval  33952  lmatval  33970  ispcmp  34014  qqhval2  34139  rrhval  34153  xrhval  34175  esumc  34208  esumpad  34212  esumpcvgval  34235  ofcfval3  34259  issiga  34269  baselsiga  34272  sigasspw  34273  issgon  34280  isrnsigau  34284  sigagenval  34297  ispisys2  34310  cldssbrsiga  34344  sxval  34347  ismeas  34356  cnmbfm  34420  mbfmcnt  34425  elcarsg  34462  sitmval  34506  eulerpartlemt0  34526  sseqval  34545  sseqmw  34548  sseqp1  34552  orvcval  34615  orvcval4  34618  ballotlemsv  34667  prcinf  35269  satf  35547  satfv1lem  35556  satefv  35608  mrexval  35695  mrsubffval  35701  msubffval  35717  mclsval  35757  eldm3  35955  opelco3  35969  elima4  35970  elfix2  36096  elsingles  36110  fvimage  36123  funpartlem  36136  elaltxp  36169  brcolinear2  36252  ellines  36346  topfneec  36549  topfneec2  36550  fnejoin2  36563  limsucncmpi  36639  findabrcl  36648  weiunse  36662  bj-ififc  36782  elelb  37098  bj-pwvrelb  37099  bj-sngltag  37184  bj-xtagex  37190  bj-elsnb  37262  bj-epelg  37269  bj-evalval  37280  bj-ismoore  37310  bj-ideqg1  37369  bj-ideqg1ALT  37370  bj-elid6  37375  bj-diagval  37379  bj-eldiag2  37382  bj-isrvec  37499  finxpreclem1  37594  finxpreclem3  37598  elghomlem2OLD  38087  isrngo  38098  isdivrngo  38151  br1cnvres  38469  riotasv2d  39227  riotasv3d  39230  lshpset  39248  lsatset  39260  lcvfbr  39290  lflset  39329  lkrfval  39357  lkrval2  39360  islshpkrN  39390  ldualset  39395  cmtfvalN  39480  cvrfval  39538  pats  39555  llnset  39775  lplnset  39799  lvolset  39842  lineset  40008  pointsetN  40011  psubspset  40014  pmapfval  40026  paddfval  40067  pclfvalN  40159  polfvalN  40174  psubclsetN  40206  watfvalN  40262  lhpset  40265  lautset  40352  pautsetN  40368  ldilfset  40378  ltrnfset  40387  dilfsetN  40422  trnfsetN  40425  trlfset  40430  tgrpfset  41014  tendofset  41028  erngfset  41069  erngfset-rN  41077  dvafset  41274  diaffval  41300  dvhfset  41350  docaffvalN  41391  djaffvalN  41403  dibffval  41410  dicffval  41444  dihffval  41500  dochffval  41619  djhffval  41666  lpolsetN  41752  lcdfval  41858  mapdffval  41896  hvmapffval  42028  hdmap1ffval  42065  hdmapffval  42096  hgmapffval  42155  hlhilset  42204  elrfi  42946  nacsfix  42964  mapfzcons2  42971  sbc2rexgOLD  43040  sbc4rexgOLD  43042  setindtrs  43277  wepwso  43295  hbtlem1  43375  hbtlem7  43377  mendval  43431  oaltublim  43542  omord2lim  43552  cnvtrucl0  43875  eliunov2  43930  iunrelexpmin1  43959  iunrelexpmin2  43963  trclfvcom  43974  cnvtrclfv  43975  trclimalb2  43977  trclfvdecomr  43979  gneispacef2  44387  gneispacern2  44390  gneispace0nelrn  44391  addrval  44716  subrval  44717  mulvval  44718  orbitclmpt  45209  elixpconstg  45343  mptfnd  45496  upbdrech  45563  climf  45878  climf2  45920  liminfval  46013  dvcosre  46166  itgsinexplem1  46208  itgsubsticclem  46229  dmvolss  46239  stoweidlem26  46280  stoweidlem35  46289  stirlinglem14  46341  fourierdlem42  46403  fourierdlem81  46441  fourierdlem89  46449  fourierdlem91  46451  salgenval  46575  elsprel  47731  sprval  47735  prprval  47770  isisubgr  48118  isgrim  48138  uhgrimisgrgric  48187  grtri  48196  isgrlim  48238  usgrexmpl2nb0  48287  usgrexmpl2nb1  48288  usgrexmpl2nb3  48290  upwlksfval  48391  isupwlkg  48393  intopval  48458  clintopval  48460  assintopval  48461  rngcvalALTV  48521  ringcvalALTV  48545  dmatbas  48659  lincop  48664  lcoop  48667  fdivval  48795  blenval  48827  itcoval  48917  itcoval1  48919  itcoval2  48920  itcoval3  48921  itcovalsucov  48924  lines  48987  spheres  49002  discsnterm  49829  termolmd  49925