Theorem elex 3478

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ∃wex 1812   ∈ wcel 2146  Vcvv 3457

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459

This theorem is used by:  elexi  3479  elexd  3480  prcnel  3482  vtoclgf  3536  vtocl2gf  3538  vtocl3gf  3539  vtocl2g  3540  vtocl3g  3541  spcgv  3557  spc3egv  3564  elab4g  3644  elrabf  3649  elrab  3652  elrab2w  3657  class2seteq  3669  mob  3682  sbcex  3756  sbcel1v  3811  sbcabel  3832  csbiebt  3883  eldif  3916  elin  3922  ssv  3962  elun  4107  csbnestgfw  4387  sbcco3gw  4390  csbnestgf  4392  sbcco3g  4395  csbco3g  4396  csbvarg  4399  sbccsb2  4402  elpwb  4572  pwidg  4584  pwidb  4586  elpr2g  4617  snidb  4629  ifpr  4661  snssg  4751  eldifvsn  4767  preqsnd  4826  elpreqpr  4834  dfopg  4838  eluni  4877  eliun  4962  csbexg  5275  nvelOLD  5287  axpweq  5323  reusv2lem4  5374  elopab  5513  epelg  5564  opelvvg  5704  opeliunxp2  5826  opelres  5986  imasng  6088  elimasni  6095  iniseg  6101  inisegn0  6102  dmmptg  6245  elon2  6375  ordsssuc2  6458  iota2  6529  fnmptf  6675  fnmpt  6679  fvelimab  6957  mpteqb  7013  fvmptt  7014  fvmptf  7015  fvopab5  7027  fvopab6  7028  fprg  7158  eloprabga  7528  ovmpos  7567  ov2gf  7568  ovmpox  7572  ovmpoga  7573  ovmpt3rab1  7678  brrpssg  7732  sorpssi  7736  elpwun  7774  ordeleqon  7787  onintrab  7801  sucexg  7810  sucexeloni  7814  ordsucelsuc  7824  onzsl  7848  dmfexALT  7911  elxp5  7926  fabexg  7941  f1oabexg  7944  offval3  7985  releldm2  8046  fnmpo  8072  mpoexg  8079  bropfvvvv  8093  fsplitfpar  8119  suppval  8164  opeliunxp2f  8212  brtpos2  8234  undefval  8279  tfr2b  8389  tz7.49  8438  oeordi  8579  relelec  8748  ecdmn0  8753  mapvalg  8839  pmvalg  8840  elpmg  8846  elixp2  8905  mptelixpg  8939  elixpsn  8941  2pwuninel  9127  ordfin  9207  rex2dom  9220  fival  9379  elfi2  9381  dffi2  9390  elfiun  9397  wemapso2lem  9521  harval  9529  brwdom  9536  fowdom  9540  brwdom2  9542  brwdom3  9551  en2lp  9582  cantnfsuc  9646  rankvalb  9776  rankwflem  9794  rankr1g  9811  r1pwALT  9825  r1rankid  9838  djulcl  9912  djurcl  9913  inlresf  9916  inrresf  9918  djuss  9922  1stinl  9929  2ndinl  9930  1stinr  9931  2ndinr  9932  cardval3  9954  dfac8alem  10029  isacn  10044  numacn  10049  acndom  10051  cardinfima  10097  unialeph  10101  ackbij1lem5  10222  cflm  10248  isf32lem2  10353  isfin1-2  10384  itunifval  10415  numth3  10469  ttukeylem1  10508  cardidg  10549  ondomon  10564  elwina  10688  elina  10689  wuncval  10744  tskmval  10841  eltskm  10845  recmulnq  10966  elnp  10989  elnpi  10990  npomex  10998  indv  12237  elfzp12  13650  seqp1  14072  hashinf  14391  hashxnn0  14395  hashnn0pnf  14398  hashxrcl  14413  prsshashgt1  14467  hashmap  14492  lsw  14621  ccatfval  14630  ccats1alpha  14679  swrdval  14703  pfxval  14735  splval  14812  splcl  14813  revval  14821  reps  14833  s3sndisj  15030  s3iunsndisj  15031  trclfv  15063  relexp0g  15085  relexpsucnnr  15088  relexp1g  15089  limsupcl  15550  limsupval  15551  clim  15571  rlim  15572  hashbcval  17086  isstruct2  17233  setsvalg  17250  setsfun0  17256  setscom  17264  strfvnd  17269  setsid  17291  ressval  17317  ressinbas  17329  restval  17503  pwsval  17563  xpsfrnel2  17642  ismre  17666  oppcval  17793  oppccatf  17808  brssc  17895  rescval  17908  issubc  17916  isfunc  17945  homadm  18121  homacd  18122  uncfval  18314  pltfval  18409  lubfval  18428  glbfval  18441  joinfval  18451  meetfval  18465  p0val  18505  p1val  18506  oduclatb  18587  ipoval  18610  pws0g  18870  frmdval  18949  vrmdfval  18954  efmnd  18968  efmnd2hash  18992  eqgfval  19290  gaid  19415  cntzfval  19436  elsymgbas  19490  symg2hash  19508  pmtrfval  19566  symggen  19586  gexval  19694  lsmfval  19754  pj1fval  19810  frgpval  19874  vrgpfval  19882  dmdprd  20116  dprdw  20128  pws1  20454  pwsmgp  20456  dvdsr  20492  isrngim  20575  rgspnval  20763  rnghmsscmap  20781  rhmsscmap  20810  lssset  21106  lspfval  21146  islbs  21249  sraval  21348  zlmval  21717  psgnevpmb  21789  ocvfval  21868  cssval  21884  thlval  21897  dsmmval  21936  dsmmbase  21937  frlmval  21950  uvcfval  21986  islinds  22011  ltbval  22246  evlsval  22289  coe1fval  22417  evls1fval  22531  matval  22620  oftpos  22661  dmatval  22701  scmatval  22713  smadiadetglem2  22881  cpmat  22918  mat2pmatfval  22932  cpm2mfval  22958  decpmatval0  22973  pm2mpval  23004  chpmatfval  23039  basdif0  23162  tgval  23164  eltg  23166  eltg2  23167  neipeltop  23338  ordtval  23398  islocfin  23727  txval  23774  qtopval  23905  isfbas  24039  isfildlem  24067  fmval  24153  fmf  24155  isfcls  24219  alexsubb  24256  tsmsfbas  24338  ustval  24413  elutop  24443  isusp  24471  ispsmet  24514  ismet  24533  isxmet  24534  blfvalps  24593  metustel  24760  tngval  24849  elpi1  25257  rrxval  25599  q1peqb  26366  ig1pval  26386  taylfval  26575  ulmval  26596  elno  27863  nosupno  27920  noetalem2  27959  nulslts  28021  oldlim  28133  negsval  28271  elz12s  28718  iscgrg  28834  isismt  28856  legval  28906  ishlg2  28924  ishlg  28927  ishpg  29094  iscgra  29173  isinag  29212  isleag  29221  iseqlg  29241  ttgval  29281  xmstrkgc  29292  cplgr2vpr  29843  vtxdgfval  29877  ewlksfval  30011  wksfval  30019  iswlkg  30023  wwlksnon  30269  wspthsnon  30270  avril1  30887  ispligb  30902  gidval  30937  isvcOLD  31004  0vfval  31031  elunop  32297  rabexgfGS  32918  disjdifprg  32993  disjdifprg2  32994  abfmpunirn  33070  rabfmpunirn  33071  hashgt1  33225  mntoval  33368  tocycval  33494  evpmval  33531  altgnsg  33535  sgnsv  33546  inftmrel  33566  isinftm  33567  resvval  33715  ellpi  33753  idlsrgval  33859  rprmval  33872  dimval  34057  dimvalfi  34058  smatfval  34251  lmatval  34269  ispcmp  34313  qqhval2  34438  rrhval  34452  xrhval  34474  esumc  34507  esumpad  34511  esumpcvgval  34534  ofcfval3  34558  issiga  34568  baselsiga  34571  sigasspw  34572  issgon  34579  isrnsigau  34583  sigagenval  34597  ispisys2  34610  cldssbrsiga  34644  sxval  34647  ismeas  34656  cnmbfm  34720  mbfmcnt  34725  elcarsg  34762  sitmval  34806  eulerpartlemt0  34826  sseqval  34845  sseqmw  34848  sseqp1  34852  orvcval  34915  orvcval4  34918  ballotlemsv  34967  acnum  35584  prcinf  35585  satf  35884  satfv1lem  35893  satefv  35945  mrexval  36032  mrsubffval  36038  msubffval  36054  mclsval  36094  eldm3  36292  opelco3  36306  elima4  36307  elfix2  36433  elsingles  36447  fvimage  36460  funpartlem  36473  elaltxp  36506  brcolinear2  36589  ellines  36683  topfneec  36925  topfneec2  36926  fnejoin2  36939  limsucncmpi  37015  findabrcl  37024  weiunse  37038  ttcwf2  37095  bj-ififc  37234  elelb  37591  bj-pwvrelb  37592  bj-sngltag  37678  bj-xtagex  37684  bj-elsnb  37756  bj-epelg  37763  bj-evalval  37776  bj-ismoore  37806  bj-ideqg1  37867  bj-ideqg1ALT  37868  bj-elid6  37873  bj-diagval  37877  bj-eldiag2  37880  bj-isrvec  37997  finxpreclem1  38094  finxpreclem3  38098  elghomlem2OLD  38597  isrngo  38608  isdivrngo  38661  br1cnvres  38983  riotasv2d  39791  riotasv3d  39794  lshpset  39812  lsatset  39824  lcvfbr  39854  lflset  39893  lkrfval  39921  lkrval2  39924  islshpkrN  39954  ldualset  39959  cmtfvalN  40044  cvrfval  40102  pats  40119  llnset  40339  lplnset  40363  lvolset  40406  lineset  40572  pointsetN  40575  psubspset  40578  pmapfval  40590  paddfval  40631  pclfvalN  40723  polfvalN  40738  psubclsetN  40770  watfvalN  40826  lhpset  40829  lautset  40916  pautsetN  40932  ldilfset  40942  ltrnfset  40951  dilfsetN  40986  trnfsetN  40989  trlfset  40994  tgrpfset  41578  tendofset  41592  erngfset  41633  erngfset-rN  41641  dvafset  41838  diaffval  41864  dvhfset  41914  docaffvalN  41955  djaffvalN  41967  dibffval  41974  dicffval  42008  dihffval  42064  dochffval  42183  djhffval  42230  lpolsetN  42316  lcdfval  42422  mapdffval  42460  hvmapffval  42592  hdmap1ffval  42629  hdmapffval  42660  hgmapffval  42719  hlhilset  42768  elrfi  43485  nacsfix  43503  mapfzcons2  43510  setindtrs  43812  wepwso  43830  hbtlem1  43910  hbtlem7  43912  mendval  43966  oaltublim  44077  omord2lim  44087  cnvtrucl0  44410  eliunov2  44465  iunrelexpmin1  44494  iunrelexpmin2  44498  trclfvcom  44509  cnvtrclfv  44510  trclimalb2  44512  trclfvdecomr  44514  gneispacef2  44922  gneispacern2  44925  gneispace0nelrn  44926  addrval  45234  subrval  45235  mulvval  45236  orbitclmpt  45727  elixpconstg  45867  mptfnd  46017  upbdrech  46084  climf  46398  climf2  46440  liminfval  46533  dvcosre  46686  itgsinexplem1  46728  itgsubsticclem  46749  dmvolss  46759  stoweidlem26  46800  stoweidlem35  46809  stirlinglem14  46861  fourierdlem42  46923  fourierdlem81  46961  fourierdlem89  46969  fourierdlem91  46971  salgenval  47095  elsprel  48284  sprval  48288  prprval  48323  isisubgr  48687  isgrim  48707  uhgrimisgrgric  48756  grtri  48765  isgrlim  48807  usgrexmpl2nb0  48856  usgrexmpl2nb1  48857  usgrexmpl2nb3  48859  upwlksfval  48960  isupwlkg  48962  intopval  49026  clintopval  49028  assintopval  49029  rngcvalALTV  49089  ringcvalALTV  49113  dmatbas  49242  lincop  49247  lcoop  49250  fdivval  49378  blenval  49410  itcoval  49500  itcoval1  49502  itcoval2  49503  itcoval3  49504  itcovalsucov  49507  lines  49570  spheres  49585  discsnterm  50411  termolmd  50507