Theorem elex 3480

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

Syntax hints:   → wi 4   = wceq 1540  ∃wex 1779   ∈ wcel 2108  Vcvv 3459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461

This theorem is referenced by:  elexi  3482  elexd  3483  prcnel  3486  spcimgfi1OLD  3527  vtoclgf  3548  vtocl2gf  3551  vtocl3gf  3552  vtocl2g  3553  vtocl3g  3554  spcgv  3575  spc3egv  3582  elab4g  3662  elrabf  3667  elrab  3671  elrab2w  3675  class2seteq  3687  mob  3700  sbcex  3775  sbcel1v  3831  sbcabel  3853  csbiebt  3903  eldif  3936  elin  3942  ssv  3983  elun  4128  csbnestgfw  4397  sbcco3gw  4400  csbnestgf  4402  sbcco3g  4405  csbco3g  4406  csbvarg  4409  sbccsb2  4412  elpwb  4583  pwidb  4596  elpr2g  4627  snidb  4637  ifpr  4669  snssg  4759  eldifvsn  4773  preqsnd  4835  elpreqpr  4843  dfopg  4847  eluni  4886  eliun  4971  csbexg  5280  nvel  5286  axpweq  5321  reusv2lem4  5371  elopab  5502  epelg  5554  opelvvg  5695  opeliunxp2  5818  opelres  5972  imasng  6071  elimasni  6078  iniseg  6084  inisegn0  6085  dmmptg  6231  elon2  6363  ordsssuc2  6444  iota2  6519  fnmptf  6673  fnmpt  6677  fvelimab  6950  mpteqb  7004  fvmptt  7005  fvmptf  7006  fvopab5  7018  fvopab6  7019  fprg  7144  eloprabga  7514  ovmpos  7553  ov2gf  7554  ovmpox  7558  ovmpoga  7559  ovmpt3rab1  7663  brrpssg  7717  sorpssi  7721  unexgOLD  7741  elpwun  7761  ordeleqon  7774  onintrab  7788  sucexg  7797  sucexeloni  7801  ordsucelsuc  7814  onzsl  7839  dmfexALT  7902  elxp5  7917  fabexg  7932  f1oabexg  7936  offval3  7979  releldm2  8040  fnmpo  8066  mpoexg  8073  mptmpoopabbrdOLDOLD  8080  bropfvvvv  8089  fsplitfpar  8115  suppval  8159  opeliunxp2f  8207  brtpos2  8229  undefval  8273  tfr2b  8408  tz7.49  8457  oeordi  8597  relelec  8764  ecdmn0  8766  mapvalg  8848  pmvalg  8849  elpmg  8855  elixp2  8913  mptelixpg  8947  elixpsn  8949  2pwuninel  9144  rex2dom  9252  fival  9422  elfi2  9424  dffi2  9433  elfiun  9440  wemapso2lem  9564  harval  9572  brwdom  9579  fowdom  9583  brwdom2  9585  brwdom3  9594  en2lp  9618  cantnfsuc  9682  rankvalb  9809  rankwflem  9827  rankr1g  9844  r1pwALT  9858  r1rankid  9871  djulcl  9922  djurcl  9923  inlresf  9926  inrresf  9928  djuss  9932  1stinl  9939  2ndinl  9940  1stinr  9941  2ndinr  9942  cardval3  9964  dfac8alem  10041  isacn  10056  numacn  10061  acndom  10063  cardinfima  10109  unialeph  10113  ackbij1lem5  10235  cflm  10262  isf32lem2  10366  isfin1-2  10397  itunifval  10428  numth3  10482  ttukeylem1  10521  cardidg  10560  ondomon  10575  elwina  10698  elina  10699  wuncval  10754  tskmval  10851  eltskm  10855  recmulnq  10976  elnp  10999  elnpi  11000  npomex  11008  elfzp12  13618  seqp1  14032  hashinf  14351  hashxnn0  14355  hashnn0pnf  14358  hashxrcl  14373  prsshashgt1  14426  hashmap  14451  lsw  14580  ccatfval  14589  ccats1alpha  14635  swrdval  14659  pfxval  14689  splval  14767  splcl  14768  revval  14776  reps  14786  s3sndisj  14984  s3iunsndisj  14985  trclfv  15017  relexp0g  15039  relexpsucnnr  15042  relexp1g  15043  limsupcl  15487  limsupval  15488  clim  15508  rlim  15509  hashbcval  17020  isstruct2  17166  setsvalg  17183  setsfun0  17189  setscom  17197  strfvnd  17202  setsid  17224  ressval  17252  ressinbas  17264  restval  17438  pwsval  17498  xpsfrnel2  17576  ismre  17600  oppcval  17723  oppccatf  17738  brssc  17825  rescval  17838  issubc  17846  isfunc  17875  homadm  18051  homacd  18052  uncfval  18244  pltfval  18339  lubfval  18358  glbfval  18371  joinfval  18381  meetfval  18395  p0val  18435  p1val  18436  oduclatb  18515  ipoval  18538  pws0g  18749  frmdval  18827  vrmdfval  18832  efmnd  18846  efmnd2hash  18870  eqgfval  19157  gaid  19280  cntzfval  19301  elsymgbas  19353  symg2hash  19371  pmtrfval  19429  symggen  19449  gexval  19557  lsmfval  19617  pj1fval  19673  frgpval  19737  vrgpfval  19745  dmdprd  19979  dprdw  19991  pws1  20283  pwsmgp  20285  dvdsr  20320  isrngim  20403  isrim0OLD  20439  rgspnval  20570  rnghmsscmap  20588  rhmsscmap  20617  lssset  20888  lspfval  20928  islbs  21032  sraval  21131  zlmval  21474  psgnevpmb  21545  ocvfval  21624  cssval  21640  thlval  21653  dsmmval  21692  dsmmbase  21693  frlmval  21706  uvcfval  21742  islinds  21767  ltbval  21999  evlsval  22042  coe1fval  22139  evls1fval  22255  matval  22347  oftpos  22388  dmatval  22428  scmatval  22440  smadiadetglem2  22608  cpmat  22645  mat2pmatfval  22659  cpm2mfval  22685  decpmatval0  22700  pm2mpval  22731  chpmatfval  22766  basdif0  22889  tgval  22891  eltg  22893  eltg2  22894  neipeltop  23065  ordtval  23125  islocfin  23453  txval  23500  qtopval  23631  isfbas  23765  isfildlem  23793  fmval  23879  fmf  23881  isfcls  23945  alexsubb  23982  tsmsfbas  24064  ustval  24139  elutop  24170  isusp  24198  ispsmet  24241  ismet  24260  isxmet  24261  blfvalps  24320  metustel  24487  tngval  24576  elpi1  24994  rrxval  25337  q1peqb  26111  ig1pval  26131  taylfval  26316  ulmval  26339  elno  27607  elnoOLD  27608  nosupno  27665  noetalem2  27704  oldlim  27842  negsval  27974  elzs12  28338  iscgrg  28437  isismt  28459  legval  28509  ishlg  28527  ishpg  28684  iscgra  28734  isinag  28763  isleag  28772  iseqlg  28792  ttgval  28800  xmstrkgc  28811  cplgr2vpr  29358  vtxdgfval  29393  ewlksfval  29527  wksfval  29535  iswlkg  29539  wwlksnon  29779  wspthsnon  29780  avril1  30390  ispligb  30404  gidval  30439  isvcOLD  30506  0vfval  30533  elunop  31799  rabexgfGS  32426  disjdifprg  32502  disjdifprg2  32503  abfmpunirn  32576  rabfmpunirn  32577  hashgt1  32733  indv  32775  mntoval  32908  tocycval  33065  evpmval  33102  altgnsg  33106  sgnsv  33117  inftmrel  33124  isinftm  33125  resvval  33291  ellpi  33334  idlsrgval  33464  rprmval  33477  dimval  33586  dimvalfi  33587  smatfval  33772  lmatval  33790  ispcmp  33834  qqhval2  33959  rrhval  33973  xrhval  33995  esumc  34028  esumpad  34032  esumpcvgval  34055  ofcfval3  34079  issiga  34089  baselsiga  34092  sigasspw  34093  issgon  34100  isrnsigau  34104  sigagenval  34117  ispisys2  34130  cldssbrsiga  34164  sxval  34167  ismeas  34176  cnmbfm  34241  mbfmcnt  34246  elcarsg  34283  sitmval  34327  eulerpartlemt0  34347  sseqval  34366  sseqmw  34369  sseqp1  34373  orvcval  34436  orvcval4  34439  ballotlemsv  34488  prcinf  35071  satf  35321  satfv1lem  35330  satefv  35382  mrexval  35469  mrsubffval  35475  msubffval  35491  mclsval  35531  eldm3  35724  opelco3  35738  elima4  35739  elfix2  35868  elsingles  35882  fvimage  35895  funpartlem  35906  elaltxp  35939  brcolinear2  36022  ellines  36116  topfneec  36319  topfneec2  36320  fnejoin2  36333  limsucncmpi  36409  findabrcl  36418  weiunse  36432  bj-ififc  36546  elelb  36861  bj-pwvrelb  36862  bj-sngltag  36947  bj-xtagex  36953  bj-elsnb  37025  bj-epelg  37032  bj-evalval  37039  bj-ismoore  37069  bj-ideqg1  37128  bj-ideqg1ALT  37129  bj-elid6  37134  bj-diagval  37138  bj-eldiag2  37141  bj-isrvec  37258  finxpreclem1  37353  finxpreclem3  37357  elghomlem2OLD  37856  isrngo  37867  isdivrngo  37920  br1cnvres  38233  riotasv2d  38921  riotasv3d  38924  lshpset  38942  lsatset  38954  lcvfbr  38984  lflset  39023  lkrfval  39051  lkrval2  39054  islshpkrN  39084  ldualset  39089  cmtfvalN  39174  cvrfval  39232  pats  39249  llnset  39470  lplnset  39494  lvolset  39537  lineset  39703  pointsetN  39706  psubspset  39709  pmapfval  39721  paddfval  39762  pclfvalN  39854  polfvalN  39869  psubclsetN  39901  watfvalN  39957  lhpset  39960  lautset  40047  pautsetN  40063  ldilfset  40073  ltrnfset  40082  dilfsetN  40117  trnfsetN  40120  trlfset  40125  tgrpfset  40709  tendofset  40723  erngfset  40764  erngfset-rN  40772  dvafset  40969  diaffval  40995  dvhfset  41045  docaffvalN  41086  djaffvalN  41098  dibffval  41105  dicffval  41139  dihffval  41195  dochffval  41314  djhffval  41361  lpolsetN  41447  lcdfval  41553  mapdffval  41591  hvmapffval  41723  hdmap1ffval  41760  hdmapffval  41791  hgmapffval  41850  hlhilset  41899  elrfi  42664  nacsfix  42682  mapfzcons2  42689  sbc2rexgOLD  42758  sbc4rexgOLD  42760  setindtrs  42996  wepwso  43014  hbtlem1  43094  hbtlem7  43096  mendval  43150  oaltublim  43261  omord2lim  43271  cnvtrucl0  43595  eliunov2  43650  iunrelexpmin1  43679  iunrelexpmin2  43683  trclfvcom  43694  cnvtrclfv  43695  trclimalb2  43697  trclfvdecomr  43699  gneispacef2  44107  gneispacern2  44110  gneispace0nelrn  44111  addrval  44438  subrval  44439  mulvval  44440  orbitclmpt  44931  elixpconstg  45061  mptfnd  45214  upbdrech  45282  climf  45599  climf2  45643  liminfval  45736  dvcosre  45889  itgsinexplem1  45931  itgsubsticclem  45952  dmvolss  45962  stoweidlem26  46003  stoweidlem35  46012  stirlinglem14  46064  fourierdlem42  46126  fourierdlem81  46164  fourierdlem89  46172  fourierdlem91  46174  salgenval  46298  elsprel  47437  sprval  47441  prprval  47476  isisubgr  47823  isgrim  47843  uhgrimisgrgric  47892  grtri  47900  isgrlim  47942  usgrexmpl2nb0  47983  usgrexmpl2nb1  47984  usgrexmpl2nb3  47986  upwlksfval  48058  isupwlkg  48060  intopval  48125  clintopval  48127  assintopval  48128  rngcvalALTV  48188  ringcvalALTV  48212  dmatbas  48327  lincop  48332  lcoop  48335  fdivval  48467  blenval  48499  itcoval  48589  itcoval1  48591  itcoval2  48592  itcoval3  48593  itcovalsucov  48596  lines  48659  spheres  48674  discsnterm  49399