Theorem elex 3457

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

Syntax hints:   → wi 4   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Vcvv 3436

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438

This theorem is referenced by:  elexi  3459  elexd  3460  prcnel  3462  spcimgfi1OLD  3503  vtoclgf  3524  vtocl2gf  3527  vtocl3gf  3528  vtocl2g  3529  vtocl3g  3530  spcgv  3551  spc3egv  3558  elab4g  3639  elrabf  3644  elrab  3648  elrab2w  3652  class2seteq  3664  mob  3677  sbcex  3752  sbcel1v  3808  sbcabel  3830  csbiebt  3880  eldif  3913  elin  3919  ssv  3960  elun  4104  csbnestgfw  4373  sbcco3gw  4376  csbnestgf  4378  sbcco3g  4381  csbco3g  4382  csbvarg  4385  sbccsb2  4388  elpwb  4559  pwidb  4572  elpr2g  4603  snidb  4613  ifpr  4645  snssg  4735  eldifvsn  4748  preqsnd  4810  elpreqpr  4818  dfopg  4822  eluni  4861  eliun  4945  csbexg  5249  nvel  5255  axpweq  5290  reusv2lem4  5340  elopab  5470  epelg  5520  opelvvg  5660  opeliunxp2  5781  opelres  5936  imasng  6035  elimasni  6042  iniseg  6048  inisegn0  6049  dmmptg  6191  elon2  6318  ordsssuc2  6400  iota2  6471  fnmptf  6618  fnmpt  6622  fvelimab  6895  mpteqb  6949  fvmptt  6950  fvmptf  6951  fvopab5  6963  fvopab6  6964  fprg  7089  eloprabga  7458  ovmpos  7497  ov2gf  7498  ovmpox  7502  ovmpoga  7503  ovmpt3rab1  7607  brrpssg  7661  sorpssi  7665  unexgOLD  7685  elpwun  7705  ordeleqon  7718  onintrab  7732  sucexg  7741  sucexeloni  7745  ordsucelsuc  7755  onzsl  7779  dmfexALT  7841  elxp5  7856  fabexg  7871  f1oabexg  7875  offval3  7917  releldm2  7978  fnmpo  8004  mpoexg  8011  bropfvvvv  8025  fsplitfpar  8051  suppval  8095  opeliunxp2f  8143  brtpos2  8165  undefval  8209  tfr2b  8318  tz7.49  8367  oeordi  8505  relelec  8672  ecdmn0  8677  mapvalg  8763  pmvalg  8764  elpmg  8770  elixp2  8828  mptelixpg  8862  elixpsn  8864  2pwuninel  9049  rex2dom  9142  fival  9302  elfi2  9304  dffi2  9313  elfiun  9320  wemapso2lem  9444  harval  9452  brwdom  9459  fowdom  9463  brwdom2  9465  brwdom3  9474  en2lp  9502  cantnfsuc  9566  rankvalb  9693  rankwflem  9711  rankr1g  9728  r1pwALT  9742  r1rankid  9755  djulcl  9806  djurcl  9807  inlresf  9810  inrresf  9812  djuss  9816  1stinl  9823  2ndinl  9824  1stinr  9825  2ndinr  9826  cardval3  9848  dfac8alem  9923  isacn  9938  numacn  9943  acndom  9945  cardinfima  9991  unialeph  9995  ackbij1lem5  10117  cflm  10144  isf32lem2  10248  isfin1-2  10279  itunifval  10310  numth3  10364  ttukeylem1  10403  cardidg  10442  ondomon  10457  elwina  10580  elina  10581  wuncval  10636  tskmval  10733  eltskm  10737  recmulnq  10858  elnp  10881  elnpi  10882  npomex  10890  elfzp12  13506  seqp1  13923  hashinf  14242  hashxnn0  14246  hashnn0pnf  14249  hashxrcl  14264  prsshashgt1  14317  hashmap  14342  lsw  14471  ccatfval  14480  ccats1alpha  14526  swrdval  14550  pfxval  14580  splval  14657  splcl  14658  revval  14666  reps  14676  s3sndisj  14874  s3iunsndisj  14875  trclfv  14907  relexp0g  14929  relexpsucnnr  14932  relexp1g  14933  limsupcl  15380  limsupval  15381  clim  15401  rlim  15402  hashbcval  16914  isstruct2  17060  setsvalg  17077  setsfun0  17083  setscom  17091  strfvnd  17096  setsid  17118  ressval  17144  ressinbas  17156  restval  17330  pwsval  17390  xpsfrnel2  17468  ismre  17492  oppcval  17619  oppccatf  17634  brssc  17721  rescval  17734  issubc  17742  isfunc  17771  homadm  17947  homacd  17948  uncfval  18140  pltfval  18235  lubfval  18254  glbfval  18267  joinfval  18277  meetfval  18291  p0val  18331  p1val  18332  oduclatb  18413  ipoval  18436  pws0g  18647  frmdval  18725  vrmdfval  18730  efmnd  18744  efmnd2hash  18768  eqgfval  19055  gaid  19178  cntzfval  19199  elsymgbas  19253  symg2hash  19271  pmtrfval  19329  symggen  19349  gexval  19457  lsmfval  19517  pj1fval  19573  frgpval  19637  vrgpfval  19645  dmdprd  19879  dprdw  19891  pws1  20210  pwsmgp  20212  dvdsr  20247  isrngim  20330  isrim0OLD  20366  rgspnval  20497  rnghmsscmap  20515  rhmsscmap  20544  lssset  20836  lspfval  20876  islbs  20980  sraval  21079  zlmval  21422  psgnevpmb  21494  ocvfval  21573  cssval  21589  thlval  21602  dsmmval  21641  dsmmbase  21642  frlmval  21655  uvcfval  21691  islinds  21716  ltbval  21948  evlsval  21991  coe1fval  22088  evls1fval  22204  matval  22296  oftpos  22337  dmatval  22377  scmatval  22389  smadiadetglem2  22557  cpmat  22594  mat2pmatfval  22608  cpm2mfval  22634  decpmatval0  22649  pm2mpval  22680  chpmatfval  22715  basdif0  22838  tgval  22840  eltg  22842  eltg2  22843  neipeltop  23014  ordtval  23074  islocfin  23402  txval  23449  qtopval  23580  isfbas  23714  isfildlem  23742  fmval  23828  fmf  23830  isfcls  23894  alexsubb  23931  tsmsfbas  24013  ustval  24088  elutop  24119  isusp  24147  ispsmet  24190  ismet  24209  isxmet  24210  blfvalps  24269  metustel  24436  tngval  24525  elpi1  24943  rrxval  25285  q1peqb  26059  ig1pval  26079  taylfval  26264  ulmval  26287  elno  27555  elnoOLD  27556  nosupno  27613  noetalem2  27652  oldlim  27801  negsval  27936  elzs12  28350  iscgrg  28457  isismt  28479  legval  28529  ishlg  28547  ishpg  28704  iscgra  28754  isinag  28783  isleag  28792  iseqlg  28812  ttgval  28820  xmstrkgc  28831  cplgr2vpr  29378  vtxdgfval  29413  ewlksfval  29547  wksfval  29555  iswlkg  29559  wwlksnon  29796  wspthsnon  29797  avril1  30407  ispligb  30421  gidval  30456  isvcOLD  30523  0vfval  30550  elunop  31816  rabexgfGS  32443  disjdifprg  32519  disjdifprg2  32520  abfmpunirn  32596  rabfmpunirn  32597  hashgt1  32754  indv  32796  mntoval  32925  tocycval  33051  evpmval  33088  altgnsg  33092  sgnsv  33103  inftmrel  33123  isinftm  33124  resvval  33268  ellpi  33311  idlsrgval  33441  rprmval  33454  dimval  33573  dimvalfi  33574  smatfval  33768  lmatval  33786  ispcmp  33830  qqhval2  33955  rrhval  33969  xrhval  33991  esumc  34024  esumpad  34028  esumpcvgval  34051  ofcfval3  34075  issiga  34085  baselsiga  34088  sigasspw  34089  issgon  34096  isrnsigau  34100  sigagenval  34113  ispisys2  34126  cldssbrsiga  34160  sxval  34163  ismeas  34172  cnmbfm  34237  mbfmcnt  34242  elcarsg  34279  sitmval  34323  eulerpartlemt0  34343  sseqval  34362  sseqmw  34365  sseqp1  34369  orvcval  34432  orvcval4  34435  ballotlemsv  34484  prcinf  35075  satf  35336  satfv1lem  35345  satefv  35397  mrexval  35484  mrsubffval  35490  msubffval  35506  mclsval  35546  eldm3  35744  opelco3  35758  elima4  35759  elfix2  35888  elsingles  35902  fvimage  35915  funpartlem  35926  elaltxp  35959  brcolinear2  36042  ellines  36136  topfneec  36339  topfneec2  36340  fnejoin2  36353  limsucncmpi  36429  findabrcl  36438  weiunse  36452  bj-ififc  36566  elelb  36881  bj-pwvrelb  36882  bj-sngltag  36967  bj-xtagex  36973  bj-elsnb  37045  bj-epelg  37052  bj-evalval  37059  bj-ismoore  37089  bj-ideqg1  37148  bj-ideqg1ALT  37149  bj-elid6  37154  bj-diagval  37158  bj-eldiag2  37161  bj-isrvec  37278  finxpreclem1  37373  finxpreclem3  37377  elghomlem2OLD  37876  isrngo  37887  isdivrngo  37940  br1cnvres  38254  riotasv2d  38946  riotasv3d  38949  lshpset  38967  lsatset  38979  lcvfbr  39009  lflset  39048  lkrfval  39076  lkrval2  39079  islshpkrN  39109  ldualset  39114  cmtfvalN  39199  cvrfval  39257  pats  39274  llnset  39494  lplnset  39518  lvolset  39561  lineset  39727  pointsetN  39730  psubspset  39733  pmapfval  39745  paddfval  39786  pclfvalN  39878  polfvalN  39893  psubclsetN  39925  watfvalN  39981  lhpset  39984  lautset  40071  pautsetN  40087  ldilfset  40097  ltrnfset  40106  dilfsetN  40141  trnfsetN  40144  trlfset  40149  tgrpfset  40733  tendofset  40747  erngfset  40788  erngfset-rN  40796  dvafset  40993  diaffval  41019  dvhfset  41069  docaffvalN  41110  djaffvalN  41122  dibffval  41129  dicffval  41163  dihffval  41219  dochffval  41338  djhffval  41385  lpolsetN  41471  lcdfval  41577  mapdffval  41615  hvmapffval  41747  hdmap1ffval  41784  hdmapffval  41815  hgmapffval  41874  hlhilset  41923  elrfi  42677  nacsfix  42695  mapfzcons2  42702  sbc2rexgOLD  42771  sbc4rexgOLD  42773  setindtrs  43008  wepwso  43026  hbtlem1  43106  hbtlem7  43108  mendval  43162  oaltublim  43273  omord2lim  43283  cnvtrucl0  43607  eliunov2  43662  iunrelexpmin1  43691  iunrelexpmin2  43695  trclfvcom  43706  cnvtrclfv  43707  trclimalb2  43709  trclfvdecomr  43711  gneispacef2  44119  gneispacern2  44122  gneispace0nelrn  44123  addrval  44449  subrval  44450  mulvval  44451  orbitclmpt  44942  elixpconstg  45077  mptfnd  45230  upbdrech  45297  climf  45613  climf2  45657  liminfval  45750  dvcosre  45903  itgsinexplem1  45945  itgsubsticclem  45966  dmvolss  45976  stoweidlem26  46017  stoweidlem35  46026  stirlinglem14  46078  fourierdlem42  46140  fourierdlem81  46178  fourierdlem89  46186  fourierdlem91  46188  salgenval  46312  elsprel  47469  sprval  47473  prprval  47508  isisubgr  47856  isgrim  47876  uhgrimisgrgric  47925  grtri  47934  isgrlim  47976  usgrexmpl2nb0  48025  usgrexmpl2nb1  48026  usgrexmpl2nb3  48028  upwlksfval  48129  isupwlkg  48131  intopval  48196  clintopval  48198  assintopval  48199  rngcvalALTV  48259  ringcvalALTV  48283  dmatbas  48398  lincop  48403  lcoop  48406  fdivval  48534  blenval  48566  itcoval  48656  itcoval1  48658  itcoval2  48659  itcoval3  48660  itcovalsucov  48663  lines  48726  spheres  48741  discsnterm  49569  termolmd  49665