Theorem elex 3450

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

Syntax hints:   → wi 4   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431

This theorem is referenced by:  elexi  3452  elexd  3453  prcnel  3455  spcimgfi1OLD  3493  vtoclgf  3513  vtocl2gf  3515  vtocl3gf  3516  vtocl2g  3517  vtocl3g  3518  spcgv  3538  spc3egv  3545  elab4g  3626  elrabf  3631  elrab  3634  elrab2w  3638  class2seteq  3650  mob  3663  sbcex  3738  sbcel1v  3794  sbcabel  3816  csbiebt  3866  eldif  3899  elin  3905  ssv  3946  elun  4093  csbnestgfw  4362  sbcco3gw  4365  csbnestgf  4367  sbcco3g  4370  csbco3g  4371  csbvarg  4374  sbccsb2  4377  elpwb  4549  pwidb  4562  elpr2g  4593  snidb  4605  ifpr  4637  snssg  4727  eldifvsn  4742  preqsnd  4802  elpreqpr  4810  dfopg  4814  eluni  4853  eliun  4937  csbexg  5245  nvelOLD  5257  axpweq  5292  reusv2lem4  5343  elopab  5482  epelg  5532  opelvvg  5672  opeliunxp2  5793  opelres  5950  imasng  6049  elimasni  6056  iniseg  6062  inisegn0  6063  dmmptg  6206  elon2  6334  ordsssuc2  6416  iota2  6487  fnmptf  6634  fnmpt  6638  fvelimab  6912  mpteqb  6967  fvmptt  6968  fvmptf  6969  fvopab5  6981  fvopab6  6982  fprg  7109  eloprabga  7476  ovmpos  7515  ov2gf  7516  ovmpox  7520  ovmpoga  7521  ovmpt3rab1  7625  brrpssg  7679  sorpssi  7683  unexgOLD  7703  elpwun  7723  ordeleqon  7736  onintrab  7750  sucexg  7759  sucexeloni  7763  ordsucelsuc  7773  onzsl  7797  dmfexALT  7859  elxp5  7874  fabexg  7889  f1oabexg  7893  offval3  7935  releldm2  7996  fnmpo  8022  mpoexg  8029  bropfvvvv  8042  fsplitfpar  8068  suppval  8112  opeliunxp2f  8160  brtpos2  8182  undefval  8226  tfr2b  8335  tz7.49  8384  oeordi  8523  relelec  8691  ecdmn0  8696  mapvalg  8783  pmvalg  8784  elpmg  8790  elixp2  8849  mptelixpg  8883  elixpsn  8885  2pwuninel  9070  ordfin  9150  rex2dom  9163  fival  9325  elfi2  9327  dffi2  9336  elfiun  9343  wemapso2lem  9467  harval  9475  brwdom  9482  fowdom  9486  brwdom2  9488  brwdom3  9497  en2lp  9527  cantnfsuc  9591  rankvalb  9721  rankwflem  9739  rankr1g  9756  r1pwALT  9770  r1rankid  9783  djulcl  9834  djurcl  9835  inlresf  9838  inrresf  9840  djuss  9844  1stinl  9851  2ndinl  9852  1stinr  9853  2ndinr  9854  cardval3  9876  dfac8alem  9951  isacn  9966  numacn  9971  acndom  9973  cardinfima  10019  unialeph  10023  ackbij1lem5  10145  cflm  10172  isf32lem2  10276  isfin1-2  10307  itunifval  10338  numth3  10392  ttukeylem1  10431  cardidg  10470  ondomon  10485  elwina  10609  elina  10610  wuncval  10665  tskmval  10762  eltskm  10766  recmulnq  10887  elnp  10910  elnpi  10911  npomex  10919  indv  12161  elfzp12  13557  seqp1  13978  hashinf  14297  hashxnn0  14301  hashnn0pnf  14304  hashxrcl  14319  prsshashgt1  14372  hashmap  14397  lsw  14526  ccatfval  14535  ccats1alpha  14582  swrdval  14606  pfxval  14636  splval  14713  splcl  14714  revval  14722  reps  14732  s3sndisj  14929  s3iunsndisj  14930  trclfv  14962  relexp0g  14984  relexpsucnnr  14987  relexp1g  14988  limsupcl  15435  limsupval  15436  clim  15456  rlim  15457  hashbcval  16973  isstruct2  17119  setsvalg  17136  setsfun0  17142  setscom  17150  strfvnd  17155  setsid  17177  ressval  17203  ressinbas  17215  restval  17389  pwsval  17449  xpsfrnel2  17528  ismre  17552  oppcval  17679  oppccatf  17694  brssc  17781  rescval  17794  issubc  17802  isfunc  17831  homadm  18007  homacd  18008  uncfval  18200  pltfval  18295  lubfval  18314  glbfval  18327  joinfval  18337  meetfval  18351  p0val  18391  p1val  18392  oduclatb  18473  ipoval  18496  pws0g  18741  frmdval  18819  vrmdfval  18824  efmnd  18838  efmnd2hash  18862  eqgfval  19151  gaid  19274  cntzfval  19295  elsymgbas  19349  symg2hash  19367  pmtrfval  19425  symggen  19445  gexval  19553  lsmfval  19613  pj1fval  19669  frgpval  19733  vrgpfval  19741  dmdprd  19975  dprdw  19987  pws1  20304  pwsmgp  20306  dvdsr  20342  isrngim  20425  rgspnval  20589  rnghmsscmap  20607  rhmsscmap  20636  lssset  20928  lspfval  20968  islbs  21071  sraval  21170  zlmval  21495  psgnevpmb  21567  ocvfval  21646  cssval  21662  thlval  21675  dsmmval  21714  dsmmbase  21715  frlmval  21728  uvcfval  21764  islinds  21789  ltbval  22021  evlsval  22064  coe1fval  22169  evls1fval  22284  matval  22376  oftpos  22417  dmatval  22457  scmatval  22469  smadiadetglem2  22637  cpmat  22674  mat2pmatfval  22688  cpm2mfval  22714  decpmatval0  22729  pm2mpval  22760  chpmatfval  22795  basdif0  22918  tgval  22920  eltg  22922  eltg2  22923  neipeltop  23094  ordtval  23154  islocfin  23482  txval  23529  qtopval  23660  isfbas  23794  isfildlem  23822  fmval  23908  fmf  23910  isfcls  23974  alexsubb  24011  tsmsfbas  24093  ustval  24168  elutop  24198  isusp  24226  ispsmet  24269  ismet  24288  isxmet  24289  blfvalps  24348  metustel  24515  tngval  24604  elpi1  25012  rrxval  25354  q1peqb  26121  ig1pval  26141  taylfval  26324  ulmval  26345  elno  27609  elnoOLD  27610  nosupno  27667  noetalem2  27706  nulslts  27767  oldlim  27879  negsval  28017  elz12s  28464  iscgrg  28580  isismt  28602  legval  28652  ishlg  28670  ishpg  28827  iscgra  28877  isinag  28906  isleag  28915  iseqlg  28935  ttgval  28943  xmstrkgc  28954  cplgr2vpr  29502  vtxdgfval  29536  ewlksfval  29670  wksfval  29678  iswlkg  29682  wwlksnon  29919  wspthsnon  29920  avril1  30533  ispligb  30548  gidval  30583  isvcOLD  30650  0vfval  30677  elunop  31943  rabexgfGS  32569  disjdifprg  32645  disjdifprg2  32646  abfmpunirn  32725  rabfmpunirn  32726  hashgt1  32881  mntoval  33042  tocycval  33169  evpmval  33206  altgnsg  33210  sgnsv  33221  inftmrel  33241  isinftm  33242  resvval  33389  ellpi  33433  idlsrgval  33563  rprmval  33576  dimval  33745  dimvalfi  33746  smatfval  33939  lmatval  33957  ispcmp  34001  qqhval2  34126  rrhval  34140  xrhval  34162  esumc  34195  esumpad  34199  esumpcvgval  34222  ofcfval3  34246  issiga  34256  baselsiga  34259  sigasspw  34260  issgon  34267  isrnsigau  34271  sigagenval  34284  ispisys2  34297  cldssbrsiga  34331  sxval  34334  ismeas  34343  cnmbfm  34407  mbfmcnt  34412  elcarsg  34449  sitmval  34493  eulerpartlemt0  34513  sseqval  34532  sseqmw  34535  sseqp1  34539  orvcval  34602  orvcval4  34605  ballotlemsv  34654  prcinf  35257  satf  35535  satfv1lem  35544  satefv  35596  mrexval  35683  mrsubffval  35689  msubffval  35705  mclsval  35745  eldm3  35943  opelco3  35957  elima4  35958  elfix2  36084  elsingles  36098  fvimage  36111  funpartlem  36124  elaltxp  36157  brcolinear2  36240  ellines  36334  topfneec  36537  topfneec2  36538  fnejoin2  36551  limsucncmpi  36627  findabrcl  36636  weiunse  36650  ttcwf2  36707  bj-ififc  36847  elelb  37204  bj-pwvrelb  37205  bj-sngltag  37290  bj-xtagex  37296  bj-elsnb  37368  bj-epelg  37375  bj-evalval  37387  bj-ismoore  37417  bj-ideqg1  37478  bj-ideqg1ALT  37479  bj-elid6  37484  bj-diagval  37488  bj-eldiag2  37491  bj-isrvec  37608  finxpreclem1  37705  finxpreclem3  37709  elghomlem2OLD  38207  isrngo  38218  isdivrngo  38271  br1cnvres  38595  riotasv2d  39403  riotasv3d  39406  lshpset  39424  lsatset  39436  lcvfbr  39466  lflset  39505  lkrfval  39533  lkrval2  39536  islshpkrN  39566  ldualset  39571  cmtfvalN  39656  cvrfval  39714  pats  39731  llnset  39951  lplnset  39975  lvolset  40018  lineset  40184  pointsetN  40187  psubspset  40190  pmapfval  40202  paddfval  40243  pclfvalN  40335  polfvalN  40350  psubclsetN  40382  watfvalN  40438  lhpset  40441  lautset  40528  pautsetN  40544  ldilfset  40554  ltrnfset  40563  dilfsetN  40598  trnfsetN  40601  trlfset  40606  tgrpfset  41190  tendofset  41204  erngfset  41245  erngfset-rN  41253  dvafset  41450  diaffval  41476  dvhfset  41526  docaffvalN  41567  djaffvalN  41579  dibffval  41586  dicffval  41620  dihffval  41676  dochffval  41795  djhffval  41842  lpolsetN  41928  lcdfval  42034  mapdffval  42072  hvmapffval  42204  hdmap1ffval  42241  hdmapffval  42272  hgmapffval  42331  hlhilset  42380  elrfi  43126  nacsfix  43144  mapfzcons2  43151  setindtrs  43453  wepwso  43471  hbtlem1  43551  hbtlem7  43553  mendval  43607  oaltublim  43718  omord2lim  43728  cnvtrucl0  44051  eliunov2  44106  iunrelexpmin1  44135  iunrelexpmin2  44139  trclfvcom  44150  cnvtrclfv  44151  trclimalb2  44153  trclfvdecomr  44155  gneispacef2  44563  gneispacern2  44566  gneispace0nelrn  44567  addrval  44892  subrval  44893  mulvval  44894  orbitclmpt  45385  elixpconstg  45519  mptfnd  45671  upbdrech  45738  climf  46052  climf2  46094  liminfval  46187  dvcosre  46340  itgsinexplem1  46382  itgsubsticclem  46403  dmvolss  46413  stoweidlem26  46454  stoweidlem35  46463  stirlinglem14  46515  fourierdlem42  46577  fourierdlem81  46615  fourierdlem89  46623  fourierdlem91  46625  salgenval  46749  elsprel  47935  sprval  47939  prprval  47974  isisubgr  48338  isgrim  48358  uhgrimisgrgric  48407  grtri  48416  isgrlim  48458  usgrexmpl2nb0  48507  usgrexmpl2nb1  48508  usgrexmpl2nb3  48510  upwlksfval  48611  isupwlkg  48613  intopval  48678  clintopval  48680  assintopval  48681  rngcvalALTV  48741  ringcvalALTV  48765  dmatbas  48879  lincop  48884  lcoop  48887  fdivval  49015  blenval  49047  itcoval  49137  itcoval1  49139  itcoval2  49140  itcoval3  49141  itcovalsucov  49144  lines  49207  spheres  49222  discsnterm  50049  termolmd  50145