Theorem elex 3465

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

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

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 3446

This theorem is referenced by:  elexi  3467  elexd  3468  prcnel  3470  spcimgfi1OLD  3511  vtoclgf  3532  vtocl2gf  3535  vtocl3gf  3536  vtocl2g  3537  vtocl3g  3538  spcgv  3559  spc3egv  3566  elab4g  3647  elrabf  3652  elrab  3656  elrab2w  3660  class2seteq  3672  mob  3685  sbcex  3760  sbcel1v  3816  sbcabel  3838  csbiebt  3888  eldif  3921  elin  3927  ssv  3968  elun  4112  csbnestgfw  4381  sbcco3gw  4384  csbnestgf  4386  sbcco3g  4389  csbco3g  4390  csbvarg  4393  sbccsb2  4396  elpwb  4567  pwidb  4580  elpr2g  4611  snidb  4621  ifpr  4653  snssg  4743  eldifvsn  4757  preqsnd  4819  elpreqpr  4827  dfopg  4831  eluni  4870  eliun  4955  csbexg  5260  nvel  5266  axpweq  5301  reusv2lem4  5351  elopab  5482  epelg  5532  opelvvg  5672  opeliunxp2  5792  opelres  5945  imasng  6044  elimasni  6051  iniseg  6057  inisegn0  6058  dmmptg  6203  elon2  6331  ordsssuc2  6413  iota2  6488  fnmptf  6636  fnmpt  6640  fvelimab  6915  mpteqb  6969  fvmptt  6970  fvmptf  6971  fvopab5  6983  fvopab6  6984  fprg  7109  eloprabga  7478  ovmpos  7517  ov2gf  7518  ovmpox  7522  ovmpoga  7523  ovmpt3rab1  7627  brrpssg  7681  sorpssi  7685  unexgOLD  7705  elpwun  7725  ordeleqon  7738  onintrab  7752  sucexg  7761  sucexeloni  7765  ordsucelsuc  7777  onzsl  7802  dmfexALT  7864  elxp5  7879  fabexg  7894  f1oabexg  7898  offval3  7940  releldm2  8001  fnmpo  8027  mpoexg  8034  bropfvvvv  8048  fsplitfpar  8074  suppval  8118  opeliunxp2f  8166  brtpos2  8188  undefval  8232  tfr2b  8341  tz7.49  8390  oeordi  8528  relelec  8695  ecdmn0  8700  mapvalg  8786  pmvalg  8787  elpmg  8793  elixp2  8851  mptelixpg  8885  elixpsn  8887  2pwuninel  9073  rex2dom  9169  fival  9339  elfi2  9341  dffi2  9350  elfiun  9357  wemapso2lem  9481  harval  9489  brwdom  9496  fowdom  9500  brwdom2  9502  brwdom3  9511  en2lp  9535  cantnfsuc  9599  rankvalb  9726  rankwflem  9744  rankr1g  9761  r1pwALT  9775  r1rankid  9788  djulcl  9839  djurcl  9840  inlresf  9843  inrresf  9845  djuss  9849  1stinl  9856  2ndinl  9857  1stinr  9858  2ndinr  9859  cardval3  9881  dfac8alem  9958  isacn  9973  numacn  9978  acndom  9980  cardinfima  10026  unialeph  10030  ackbij1lem5  10152  cflm  10179  isf32lem2  10283  isfin1-2  10314  itunifval  10345  numth3  10399  ttukeylem1  10438  cardidg  10477  ondomon  10492  elwina  10615  elina  10616  wuncval  10671  tskmval  10768  eltskm  10772  recmulnq  10893  elnp  10916  elnpi  10917  npomex  10925  elfzp12  13540  seqp1  13957  hashinf  14276  hashxnn0  14280  hashnn0pnf  14283  hashxrcl  14298  prsshashgt1  14351  hashmap  14376  lsw  14505  ccatfval  14514  ccats1alpha  14560  swrdval  14584  pfxval  14614  splval  14692  splcl  14693  revval  14701  reps  14711  s3sndisj  14909  s3iunsndisj  14910  trclfv  14942  relexp0g  14964  relexpsucnnr  14967  relexp1g  14968  limsupcl  15415  limsupval  15416  clim  15436  rlim  15437  hashbcval  16949  isstruct2  17095  setsvalg  17112  setsfun0  17118  setscom  17126  strfvnd  17131  setsid  17153  ressval  17179  ressinbas  17191  restval  17365  pwsval  17425  xpsfrnel2  17503  ismre  17527  oppcval  17654  oppccatf  17669  brssc  17756  rescval  17769  issubc  17777  isfunc  17806  homadm  17982  homacd  17983  uncfval  18175  pltfval  18270  lubfval  18289  glbfval  18302  joinfval  18312  meetfval  18326  p0val  18366  p1val  18367  oduclatb  18448  ipoval  18471  pws0g  18682  frmdval  18760  vrmdfval  18765  efmnd  18779  efmnd2hash  18803  eqgfval  19090  gaid  19213  cntzfval  19234  elsymgbas  19288  symg2hash  19306  pmtrfval  19364  symggen  19384  gexval  19492  lsmfval  19552  pj1fval  19608  frgpval  19672  vrgpfval  19680  dmdprd  19914  dprdw  19926  pws1  20245  pwsmgp  20247  dvdsr  20282  isrngim  20365  isrim0OLD  20401  rgspnval  20532  rnghmsscmap  20550  rhmsscmap  20579  lssset  20871  lspfval  20911  islbs  21015  sraval  21114  zlmval  21457  psgnevpmb  21529  ocvfval  21608  cssval  21624  thlval  21637  dsmmval  21676  dsmmbase  21677  frlmval  21690  uvcfval  21726  islinds  21751  ltbval  21983  evlsval  22026  coe1fval  22123  evls1fval  22239  matval  22331  oftpos  22372  dmatval  22412  scmatval  22424  smadiadetglem2  22592  cpmat  22629  mat2pmatfval  22643  cpm2mfval  22669  decpmatval0  22684  pm2mpval  22715  chpmatfval  22750  basdif0  22873  tgval  22875  eltg  22877  eltg2  22878  neipeltop  23049  ordtval  23109  islocfin  23437  txval  23484  qtopval  23615  isfbas  23749  isfildlem  23777  fmval  23863  fmf  23865  isfcls  23929  alexsubb  23966  tsmsfbas  24048  ustval  24123  elutop  24154  isusp  24182  ispsmet  24225  ismet  24244  isxmet  24245  blfvalps  24304  metustel  24471  tngval  24560  elpi1  24978  rrxval  25320  q1peqb  26094  ig1pval  26114  taylfval  26299  ulmval  26322  elno  27590  elnoOLD  27591  nosupno  27648  noetalem2  27687  oldlim  27836  negsval  27971  elzs12  28385  iscgrg  28492  isismt  28514  legval  28564  ishlg  28582  ishpg  28739  iscgra  28789  isinag  28818  isleag  28827  iseqlg  28847  ttgval  28855  xmstrkgc  28866  cplgr2vpr  29413  vtxdgfval  29448  ewlksfval  29582  wksfval  29590  iswlkg  29594  wwlksnon  29831  wspthsnon  29832  avril1  30442  ispligb  30456  gidval  30491  isvcOLD  30558  0vfval  30585  elunop  31851  rabexgfGS  32478  disjdifprg  32554  disjdifprg2  32555  abfmpunirn  32626  rabfmpunirn  32627  hashgt1  32783  indv  32825  mntoval  32954  tocycval  33080  evpmval  33117  altgnsg  33121  sgnsv  33132  inftmrel  33149  isinftm  33150  resvval  33294  ellpi  33337  idlsrgval  33467  rprmval  33480  dimval  33589  dimvalfi  33590  smatfval  33778  lmatval  33796  ispcmp  33840  qqhval2  33965  rrhval  33979  xrhval  34001  esumc  34034  esumpad  34038  esumpcvgval  34061  ofcfval3  34085  issiga  34095  baselsiga  34098  sigasspw  34099  issgon  34106  isrnsigau  34110  sigagenval  34123  ispisys2  34136  cldssbrsiga  34170  sxval  34173  ismeas  34182  cnmbfm  34247  mbfmcnt  34252  elcarsg  34289  sitmval  34333  eulerpartlemt0  34353  sseqval  34372  sseqmw  34375  sseqp1  34379  orvcval  34442  orvcval4  34445  ballotlemsv  34494  prcinf  35077  satf  35333  satfv1lem  35342  satefv  35394  mrexval  35481  mrsubffval  35487  msubffval  35503  mclsval  35543  eldm3  35741  opelco3  35755  elima4  35756  elfix2  35885  elsingles  35899  fvimage  35912  funpartlem  35923  elaltxp  35956  brcolinear2  36039  ellines  36133  topfneec  36336  topfneec2  36337  fnejoin2  36350  limsucncmpi  36426  findabrcl  36435  weiunse  36449  bj-ififc  36563  elelb  36878  bj-pwvrelb  36879  bj-sngltag  36964  bj-xtagex  36970  bj-elsnb  37042  bj-epelg  37049  bj-evalval  37056  bj-ismoore  37086  bj-ideqg1  37145  bj-ideqg1ALT  37146  bj-elid6  37151  bj-diagval  37155  bj-eldiag2  37158  bj-isrvec  37275  finxpreclem1  37370  finxpreclem3  37374  elghomlem2OLD  37873  isrngo  37884  isdivrngo  37937  br1cnvres  38251  riotasv2d  38943  riotasv3d  38946  lshpset  38964  lsatset  38976  lcvfbr  39006  lflset  39045  lkrfval  39073  lkrval2  39076  islshpkrN  39106  ldualset  39111  cmtfvalN  39196  cvrfval  39254  pats  39271  llnset  39492  lplnset  39516  lvolset  39559  lineset  39725  pointsetN  39728  psubspset  39731  pmapfval  39743  paddfval  39784  pclfvalN  39876  polfvalN  39891  psubclsetN  39923  watfvalN  39979  lhpset  39982  lautset  40069  pautsetN  40085  ldilfset  40095  ltrnfset  40104  dilfsetN  40139  trnfsetN  40142  trlfset  40147  tgrpfset  40731  tendofset  40745  erngfset  40786  erngfset-rN  40794  dvafset  40991  diaffval  41017  dvhfset  41067  docaffvalN  41108  djaffvalN  41120  dibffval  41127  dicffval  41161  dihffval  41217  dochffval  41336  djhffval  41383  lpolsetN  41469  lcdfval  41575  mapdffval  41613  hvmapffval  41745  hdmap1ffval  41782  hdmapffval  41813  hgmapffval  41872  hlhilset  41921  elrfi  42675  nacsfix  42693  mapfzcons2  42700  sbc2rexgOLD  42769  sbc4rexgOLD  42771  setindtrs  43007  wepwso  43025  hbtlem1  43105  hbtlem7  43107  mendval  43161  oaltublim  43272  omord2lim  43282  cnvtrucl0  43606  eliunov2  43661  iunrelexpmin1  43690  iunrelexpmin2  43694  trclfvcom  43705  cnvtrclfv  43706  trclimalb2  43708  trclfvdecomr  43710  gneispacef2  44118  gneispacern2  44121  gneispace0nelrn  44122  addrval  44448  subrval  44449  mulvval  44450  orbitclmpt  44941  elixpconstg  45076  mptfnd  45229  upbdrech  45296  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  47855  isgrim  47875  uhgrimisgrgric  47924  grtri  47932  isgrlim  47974  usgrexmpl2nb0  48015  usgrexmpl2nb1  48016  usgrexmpl2nb3  48018  upwlksfval  48116  isupwlkg  48118  intopval  48183  clintopval  48185  assintopval  48186  rngcvalALTV  48246  ringcvalALTV  48270  dmatbas  48385  lincop  48390  lcoop  48393  fdivval  48521  blenval  48553  itcoval  48643  itcoval1  48645  itcoval2  48646  itcoval3  48647  itcovalsucov  48650  lines  48713  spheres  48728  discsnterm  49556  termolmd  49652