Theorem elex 3476

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 2844	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
2		isset 3469	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
3	1, 2	sylibr 237	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1570  ∃wex 1809   ∈ wcel 2143  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457

This theorem is referenced by:  elexi  3477  elexd  3478  prcnel  3480  vtoclgf  3534  vtocl2gf  3536  vtocl3gf  3537  vtocl2g  3538  vtocl3g  3539  spcgv  3555  spc3egv  3562  elab4g  3642  elrabf  3647  elrab  3650  elrab2w  3655  class2seteq  3667  mob  3680  sbcex  3754  sbcel1v  3809  sbcabel  3831  csbiebt  3882  eldif  3915  elin  3921  ssv  3961  elun  4107  csbnestgfw  4387  sbcco3gw  4390  csbnestgf  4392  sbcco3g  4395  csbco3g  4396  csbvarg  4399  sbccsb2  4402  elpwb  4570  pwidg  4582  pwidb  4584  elpr2g  4615  snidb  4627  ifpr  4659  snssg  4749  eldifvsn  4765  preqsnd  4824  elpreqpr  4832  dfopg  4836  eluni  4875  eliun  4960  csbexg  5273  nvelOLD  5285  axpweq  5321  reusv2lem4  5372  elopab  5511  epelg  5562  opelvvg  5702  opeliunxp2  5824  opelres  5984  imasng  6086  elimasni  6093  iniseg  6099  inisegn0  6100  dmmptg  6243  elon2  6371  ordsssuc2  6454  iota2  6525  fnmptf  6671  fnmpt  6675  fvelimab  6953  mpteqb  7009  fvmptt  7010  fvmptf  7011  fvopab5  7023  fvopab6  7024  fprg  7152  eloprabga  7519  ovmpos  7558  ov2gf  7559  ovmpox  7563  ovmpoga  7564  ovmpt3rab1  7668  brrpssg  7722  sorpssi  7726  elpwun  7764  ordeleqon  7777  onintrab  7791  sucexg  7800  sucexeloni  7804  ordsucelsuc  7814  onzsl  7838  dmfexALT  7901  elxp5  7916  fabexg  7931  f1oabexg  7934  offval3  7975  releldm2  8036  fnmpo  8062  mpoexg  8069  bropfvvvv  8083  fsplitfpar  8109  suppval  8154  opeliunxp2f  8202  brtpos2  8224  undefval  8269  tfr2b  8379  tz7.49  8428  oeordi  8569  relelec  8738  ecdmn0  8743  mapvalg  8829  pmvalg  8830  elpmg  8836  elixp2  8895  mptelixpg  8929  elixpsn  8931  2pwuninel  9116  ordfin  9196  rex2dom  9209  fival  9368  elfi2  9370  dffi2  9379  elfiun  9386  wemapso2lem  9510  harval  9518  brwdom  9525  fowdom  9529  brwdom2  9531  brwdom3  9540  en2lp  9571  cantnfsuc  9635  rankvalb  9765  rankwflem  9783  rankr1g  9800  r1pwALT  9814  r1rankid  9827  djulcl  9892  djurcl  9893  inlresf  9896  inrresf  9898  djuss  9902  1stinl  9909  2ndinl  9910  1stinr  9911  2ndinr  9912  cardval3  9934  dfac8alem  10009  isacn  10024  numacn  10029  acndom  10031  cardinfima  10077  unialeph  10081  ackbij1lem5  10202  cflm  10228  isf32lem2  10333  isfin1-2  10364  itunifval  10395  numth3  10449  ttukeylem1  10488  cardidg  10527  ondomon  10542  elwina  10666  elina  10667  wuncval  10722  tskmval  10819  eltskm  10823  recmulnq  10944  elnp  10967  elnpi  10968  npomex  10976  indv  12215  elfzp12  13627  seqp1  14048  hashinf  14367  hashxnn0  14371  hashnn0pnf  14374  hashxrcl  14389  prsshashgt1  14443  hashmap  14468  lsw  14597  ccatfval  14606  ccats1alpha  14653  swrdval  14677  pfxval  14707  splval  14784  splcl  14785  revval  14793  reps  14803  s3sndisj  15000  s3iunsndisj  15001  trclfv  15033  relexp0g  15055  relexpsucnnr  15058  relexp1g  15059  limsupcl  15520  limsupval  15521  clim  15541  rlim  15542  hashbcval  17057  isstruct2  17204  setsvalg  17221  setsfun0  17227  setscom  17235  strfvnd  17240  setsid  17262  ressval  17288  ressinbas  17300  restval  17474  pwsval  17534  xpsfrnel2  17613  ismre  17637  oppcval  17764  oppccatf  17779  brssc  17866  rescval  17879  issubc  17887  isfunc  17916  homadm  18092  homacd  18093  uncfval  18285  pltfval  18380  lubfval  18399  glbfval  18412  joinfval  18422  meetfval  18436  p0val  18476  p1val  18477  oduclatb  18558  ipoval  18581  pws0g  18826  frmdval  18905  vrmdfval  18910  efmnd  18924  efmnd2hash  18948  eqgfval  19239  gaid  19364  cntzfval  19385  elsymgbas  19439  symg2hash  19457  pmtrfval  19515  symggen  19535  gexval  19643  lsmfval  19703  pj1fval  19759  frgpval  19823  vrgpfval  19831  dmdprd  20065  dprdw  20077  pws1  20402  pwsmgp  20404  dvdsr  20440  isrngim  20523  rgspnval  20711  rnghmsscmap  20729  rhmsscmap  20758  lssset  21054  lspfval  21094  islbs  21197  sraval  21296  zlmval  21665  psgnevpmb  21737  ocvfval  21816  cssval  21832  thlval  21845  dsmmval  21884  dsmmbase  21885  frlmval  21898  uvcfval  21934  islinds  21959  ltbval  22194  evlsval  22237  coe1fval  22365  evls1fval  22479  matval  22568  oftpos  22609  dmatval  22649  scmatval  22661  smadiadetglem2  22829  cpmat  22866  mat2pmatfval  22880  cpm2mfval  22906  decpmatval0  22921  pm2mpval  22952  chpmatfval  22987  basdif0  23110  tgval  23112  eltg  23114  eltg2  23115  neipeltop  23286  ordtval  23346  islocfin  23674  txval  23721  qtopval  23852  isfbas  23986  isfildlem  24014  fmval  24100  fmf  24102  isfcls  24166  alexsubb  24203  tsmsfbas  24285  ustval  24360  elutop  24390  isusp  24418  ispsmet  24461  ismet  24480  isxmet  24481  blfvalps  24540  metustel  24707  tngval  24796  elpi1  25204  rrxval  25546  q1peqb  26313  ig1pval  26333  taylfval  26522  ulmval  26543  elno  27810  nosupno  27867  noetalem2  27906  nulslts  27968  oldlim  28080  negsval  28218  elz12s  28665  iscgrg  28781  isismt  28803  legval  28853  ishlg2  28871  ishlg  28874  ishpg  29041  iscgra  29120  isinag  29155  isleag  29164  iseqlg  29184  ttgval  29224  xmstrkgc  29235  cplgr2vpr  29783  vtxdgfval  29817  ewlksfval  29951  wksfval  29959  iswlkg  29963  wwlksnon  30200  wspthsnon  30201  avril1  30814  ispligb  30829  gidval  30864  isvcOLD  30931  0vfval  30958  elunop  32224  rabexgfGS  32845  disjdifprg  32920  disjdifprg2  32921  abfmpunirn  32997  rabfmpunirn  32998  hashgt1  33153  mntoval  33302  tocycval  33428  evpmval  33465  altgnsg  33469  sgnsv  33480  inftmrel  33500  isinftm  33501  resvval  33649  ellpi  33687  idlsrgval  33793  rprmval  33806  dimval  33991  dimvalfi  33992  smatfval  34185  lmatval  34203  ispcmp  34247  qqhval2  34372  rrhval  34386  xrhval  34408  esumc  34441  esumpad  34445  esumpcvgval  34468  ofcfval3  34492  issiga  34502  baselsiga  34505  sigasspw  34506  issgon  34513  isrnsigau  34517  sigagenval  34530  ispisys2  34543  cldssbrsiga  34577  sxval  34580  ismeas  34589  cnmbfm  34653  mbfmcnt  34658  elcarsg  34695  sitmval  34739  eulerpartlemt0  34759  sseqval  34778  sseqmw  34781  sseqp1  34785  orvcval  34848  orvcval4  34851  ballotlemsv  34900  acnum  35525  prcinf  35526  satf  35845  satfv1lem  35854  satefv  35906  mrexval  35993  mrsubffval  35999  msubffval  36015  mclsval  36055  eldm3  36253  opelco3  36267  elima4  36268  elfix2  36394  elsingles  36408  fvimage  36421  funpartlem  36434  elaltxp  36467  brcolinear2  36550  ellines  36644  topfneec  36886  topfneec2  36887  fnejoin2  36900  limsucncmpi  36976  findabrcl  36985  weiunse  36999  ttcwf2  37056  bj-ififc  37195  elelb  37552  bj-pwvrelb  37553  bj-sngltag  37639  bj-xtagex  37645  bj-elsnb  37717  bj-epelg  37724  bj-evalval  37737  bj-ismoore  37767  bj-ideqg1  37828  bj-ideqg1ALT  37829  bj-elid6  37834  bj-diagval  37838  bj-eldiag2  37841  bj-isrvec  37958  finxpreclem1  38055  finxpreclem3  38059  elghomlem2OLD  38557  isrngo  38568  isdivrngo  38621  br1cnvres  38943  riotasv2d  39751  riotasv3d  39754  lshpset  39772  lsatset  39784  lcvfbr  39814  lflset  39853  lkrfval  39881  lkrval2  39884  islshpkrN  39914  ldualset  39919  cmtfvalN  40004  cvrfval  40062  pats  40079  llnset  40299  lplnset  40323  lvolset  40366  lineset  40532  pointsetN  40535  psubspset  40538  pmapfval  40550  paddfval  40591  pclfvalN  40683  polfvalN  40698  psubclsetN  40730  watfvalN  40786  lhpset  40789  lautset  40876  pautsetN  40892  ldilfset  40902  ltrnfset  40911  dilfsetN  40946  trnfsetN  40949  trlfset  40954  tgrpfset  41538  tendofset  41552  erngfset  41593  erngfset-rN  41601  dvafset  41798  diaffval  41824  dvhfset  41874  docaffvalN  41915  djaffvalN  41927  dibffval  41934  dicffval  41968  dihffval  42024  dochffval  42143  djhffval  42190  lpolsetN  42276  lcdfval  42382  mapdffval  42420  hvmapffval  42552  hdmap1ffval  42589  hdmapffval  42620  hgmapffval  42679  hlhilset  42728  elrfi  43445  nacsfix  43463  mapfzcons2  43470  setindtrs  43772  wepwso  43790  hbtlem1  43870  hbtlem7  43872  mendval  43926  oaltublim  44037  omord2lim  44047  cnvtrucl0  44370  eliunov2  44425  iunrelexpmin1  44454  iunrelexpmin2  44458  trclfvcom  44469  cnvtrclfv  44470  trclimalb2  44472  trclfvdecomr  44474  gneispacef2  44882  gneispacern2  44885  gneispace0nelrn  44886  addrval  45194  subrval  45195  mulvval  45196  orbitclmpt  45687  elixpconstg  45827  mptfnd  45977  upbdrech  46044  climf  46358  climf2  46400  liminfval  46493  dvcosre  46646  itgsinexplem1  46688  itgsubsticclem  46709  dmvolss  46719  stoweidlem26  46760  stoweidlem35  46769  stirlinglem14  46821  fourierdlem42  46883  fourierdlem81  46921  fourierdlem89  46929  fourierdlem91  46931  salgenval  47055  elsprel  48244  sprval  48248  prprval  48283  isisubgr  48647  isgrim  48667  uhgrimisgrgric  48716  grtri  48725  isgrlim  48767  usgrexmpl2nb0  48816  usgrexmpl2nb1  48817  usgrexmpl2nb3  48819  upwlksfval  48920  isupwlkg  48922  intopval  48987  clintopval  48989  assintopval  48990  rngcvalALTV  49050  ringcvalALTV  49074  dmatbas  49203  lincop  49208  lcoop  49211  fdivval  49339  blenval  49371  itcoval  49461  itcoval1  49463  itcoval2  49464  itcoval3  49465  itcovalsucov  49468  lines  49531  spheres  49546  discsnterm  50372  termolmd  50468