Theorem elex 3468

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

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

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 3449

This theorem is referenced by:  elexi  3470  elexd  3471  prcnel  3473  spcimgfi1OLD  3514  vtoclgf  3535  vtocl2gf  3538  vtocl3gf  3539  vtocl2g  3540  vtocl3g  3541  spcgv  3562  spc3egv  3569  elab4g  3650  elrabf  3655  elrab  3659  elrab2w  3663  class2seteq  3675  mob  3688  sbcex  3763  sbcel1v  3819  sbcabel  3841  csbiebt  3891  eldif  3924  elin  3930  ssv  3971  elun  4116  csbnestgfw  4385  sbcco3gw  4388  csbnestgf  4390  sbcco3g  4393  csbco3g  4394  csbvarg  4397  sbccsb2  4400  elpwb  4571  pwidb  4584  elpr2g  4615  snidb  4625  ifpr  4657  snssg  4747  eldifvsn  4761  preqsnd  4823  elpreqpr  4831  dfopg  4835  eluni  4874  eliun  4959  csbexg  5265  nvel  5271  axpweq  5306  reusv2lem4  5356  elopab  5487  epelg  5539  opelvvg  5679  opeliunxp2  5802  opelres  5956  imasng  6055  elimasni  6062  iniseg  6068  inisegn0  6069  dmmptg  6215  elon2  6343  ordsssuc2  6425  iota2  6500  fnmptf  6654  fnmpt  6658  fvelimab  6933  mpteqb  6987  fvmptt  6988  fvmptf  6989  fvopab5  7001  fvopab6  7002  fprg  7127  eloprabga  7498  ovmpos  7537  ov2gf  7538  ovmpox  7542  ovmpoga  7543  ovmpt3rab1  7647  brrpssg  7701  sorpssi  7705  unexgOLD  7725  elpwun  7745  ordeleqon  7758  onintrab  7772  sucexg  7781  sucexeloni  7785  ordsucelsuc  7797  onzsl  7822  dmfexALT  7884  elxp5  7899  fabexg  7914  f1oabexg  7918  offval3  7961  releldm2  8022  fnmpo  8048  mpoexg  8055  mptmpoopabbrdOLDOLD  8062  bropfvvvv  8071  fsplitfpar  8097  suppval  8141  opeliunxp2f  8189  brtpos2  8211  undefval  8255  tfr2b  8364  tz7.49  8413  oeordi  8551  relelec  8718  ecdmn0  8723  mapvalg  8809  pmvalg  8810  elpmg  8816  elixp2  8874  mptelixpg  8908  elixpsn  8910  2pwuninel  9096  rex2dom  9193  fival  9363  elfi2  9365  dffi2  9374  elfiun  9381  wemapso2lem  9505  harval  9513  brwdom  9520  fowdom  9524  brwdom2  9526  brwdom3  9535  en2lp  9559  cantnfsuc  9623  rankvalb  9750  rankwflem  9768  rankr1g  9785  r1pwALT  9799  r1rankid  9812  djulcl  9863  djurcl  9864  inlresf  9867  inrresf  9869  djuss  9873  1stinl  9880  2ndinl  9881  1stinr  9882  2ndinr  9883  cardval3  9905  dfac8alem  9982  isacn  9997  numacn  10002  acndom  10004  cardinfima  10050  unialeph  10054  ackbij1lem5  10176  cflm  10203  isf32lem2  10307  isfin1-2  10338  itunifval  10369  numth3  10423  ttukeylem1  10462  cardidg  10501  ondomon  10516  elwina  10639  elina  10640  wuncval  10695  tskmval  10792  eltskm  10796  recmulnq  10917  elnp  10940  elnpi  10941  npomex  10949  elfzp12  13564  seqp1  13981  hashinf  14300  hashxnn0  14304  hashnn0pnf  14307  hashxrcl  14322  prsshashgt1  14375  hashmap  14400  lsw  14529  ccatfval  14538  ccats1alpha  14584  swrdval  14608  pfxval  14638  splval  14716  splcl  14717  revval  14725  reps  14735  s3sndisj  14933  s3iunsndisj  14934  trclfv  14966  relexp0g  14988  relexpsucnnr  14991  relexp1g  14992  limsupcl  15439  limsupval  15440  clim  15460  rlim  15461  hashbcval  16973  isstruct2  17119  setsvalg  17136  setsfun0  17142  setscom  17150  strfvnd  17155  setsid  17177  ressval  17203  ressinbas  17215  restval  17389  pwsval  17449  xpsfrnel2  17527  ismre  17551  oppcval  17674  oppccatf  17689  brssc  17776  rescval  17789  issubc  17797  isfunc  17826  homadm  18002  homacd  18003  uncfval  18195  pltfval  18290  lubfval  18309  glbfval  18322  joinfval  18332  meetfval  18346  p0val  18386  p1val  18387  oduclatb  18466  ipoval  18489  pws0g  18700  frmdval  18778  vrmdfval  18783  efmnd  18797  efmnd2hash  18821  eqgfval  19108  gaid  19231  cntzfval  19252  elsymgbas  19304  symg2hash  19322  pmtrfval  19380  symggen  19400  gexval  19508  lsmfval  19568  pj1fval  19624  frgpval  19688  vrgpfval  19696  dmdprd  19930  dprdw  19942  pws1  20234  pwsmgp  20236  dvdsr  20271  isrngim  20354  isrim0OLD  20390  rgspnval  20521  rnghmsscmap  20539  rhmsscmap  20568  lssset  20839  lspfval  20879  islbs  20983  sraval  21082  zlmval  21425  psgnevpmb  21496  ocvfval  21575  cssval  21591  thlval  21604  dsmmval  21643  dsmmbase  21644  frlmval  21657  uvcfval  21693  islinds  21718  ltbval  21950  evlsval  21993  coe1fval  22090  evls1fval  22206  matval  22298  oftpos  22339  dmatval  22379  scmatval  22391  smadiadetglem2  22559  cpmat  22596  mat2pmatfval  22610  cpm2mfval  22636  decpmatval0  22651  pm2mpval  22682  chpmatfval  22717  basdif0  22840  tgval  22842  eltg  22844  eltg2  22845  neipeltop  23016  ordtval  23076  islocfin  23404  txval  23451  qtopval  23582  isfbas  23716  isfildlem  23744  fmval  23830  fmf  23832  isfcls  23896  alexsubb  23933  tsmsfbas  24015  ustval  24090  elutop  24121  isusp  24149  ispsmet  24192  ismet  24211  isxmet  24212  blfvalps  24271  metustel  24438  tngval  24527  elpi1  24945  rrxval  25287  q1peqb  26061  ig1pval  26081  taylfval  26266  ulmval  26289  elno  27557  elnoOLD  27558  nosupno  27615  noetalem2  27654  oldlim  27798  negsval  27931  elzs12  28337  iscgrg  28439  isismt  28461  legval  28511  ishlg  28529  ishpg  28686  iscgra  28736  isinag  28765  isleag  28774  iseqlg  28794  ttgval  28802  xmstrkgc  28813  cplgr2vpr  29360  vtxdgfval  29395  ewlksfval  29529  wksfval  29537  iswlkg  29541  wwlksnon  29781  wspthsnon  29782  avril1  30392  ispligb  30406  gidval  30441  isvcOLD  30508  0vfval  30535  elunop  31801  rabexgfGS  32428  disjdifprg  32504  disjdifprg2  32505  abfmpunirn  32576  rabfmpunirn  32577  hashgt1  32733  indv  32775  mntoval  32908  tocycval  33065  evpmval  33102  altgnsg  33106  sgnsv  33117  inftmrel  33134  isinftm  33135  resvval  33301  ellpi  33344  idlsrgval  33474  rprmval  33487  dimval  33596  dimvalfi  33597  smatfval  33785  lmatval  33803  ispcmp  33847  qqhval2  33972  rrhval  33986  xrhval  34008  esumc  34041  esumpad  34045  esumpcvgval  34068  ofcfval3  34092  issiga  34102  baselsiga  34105  sigasspw  34106  issgon  34113  isrnsigau  34117  sigagenval  34130  ispisys2  34143  cldssbrsiga  34177  sxval  34180  ismeas  34189  cnmbfm  34254  mbfmcnt  34259  elcarsg  34296  sitmval  34340  eulerpartlemt0  34360  sseqval  34379  sseqmw  34382  sseqp1  34386  orvcval  34449  orvcval4  34452  ballotlemsv  34501  prcinf  35084  satf  35340  satfv1lem  35349  satefv  35401  mrexval  35488  mrsubffval  35494  msubffval  35510  mclsval  35550  eldm3  35748  opelco3  35762  elima4  35763  elfix2  35892  elsingles  35906  fvimage  35919  funpartlem  35930  elaltxp  35963  brcolinear2  36046  ellines  36140  topfneec  36343  topfneec2  36344  fnejoin2  36357  limsucncmpi  36433  findabrcl  36442  weiunse  36456  bj-ififc  36570  elelb  36885  bj-pwvrelb  36886  bj-sngltag  36971  bj-xtagex  36977  bj-elsnb  37049  bj-epelg  37056  bj-evalval  37063  bj-ismoore  37093  bj-ideqg1  37152  bj-ideqg1ALT  37153  bj-elid6  37158  bj-diagval  37162  bj-eldiag2  37165  bj-isrvec  37282  finxpreclem1  37377  finxpreclem3  37381  elghomlem2OLD  37880  isrngo  37891  isdivrngo  37944  br1cnvres  38258  riotasv2d  38950  riotasv3d  38953  lshpset  38971  lsatset  38983  lcvfbr  39013  lflset  39052  lkrfval  39080  lkrval2  39083  islshpkrN  39113  ldualset  39118  cmtfvalN  39203  cvrfval  39261  pats  39278  llnset  39499  lplnset  39523  lvolset  39566  lineset  39732  pointsetN  39735  psubspset  39738  pmapfval  39750  paddfval  39791  pclfvalN  39883  polfvalN  39898  psubclsetN  39930  watfvalN  39986  lhpset  39989  lautset  40076  pautsetN  40092  ldilfset  40102  ltrnfset  40111  dilfsetN  40146  trnfsetN  40149  trlfset  40154  tgrpfset  40738  tendofset  40752  erngfset  40793  erngfset-rN  40801  dvafset  40998  diaffval  41024  dvhfset  41074  docaffvalN  41115  djaffvalN  41127  dibffval  41134  dicffval  41168  dihffval  41224  dochffval  41343  djhffval  41390  lpolsetN  41476  lcdfval  41582  mapdffval  41620  hvmapffval  41752  hdmap1ffval  41789  hdmapffval  41820  hgmapffval  41879  hlhilset  41928  elrfi  42682  nacsfix  42700  mapfzcons2  42707  sbc2rexgOLD  42776  sbc4rexgOLD  42778  setindtrs  43014  wepwso  43032  hbtlem1  43112  hbtlem7  43114  mendval  43168  oaltublim  43279  omord2lim  43289  cnvtrucl0  43613  eliunov2  43668  iunrelexpmin1  43697  iunrelexpmin2  43701  trclfvcom  43712  cnvtrclfv  43713  trclimalb2  43715  trclfvdecomr  43717  gneispacef2  44125  gneispacern2  44128  gneispace0nelrn  44129  addrval  44455  subrval  44456  mulvval  44457  orbitclmpt  44948  elixpconstg  45083  mptfnd  45236  upbdrech  45303  climf  45620  climf2  45664  liminfval  45757  dvcosre  45910  itgsinexplem1  45952  itgsubsticclem  45973  dmvolss  45983  stoweidlem26  46024  stoweidlem35  46033  stirlinglem14  46085  fourierdlem42  46147  fourierdlem81  46185  fourierdlem89  46193  fourierdlem91  46195  salgenval  46319  elsprel  47476  sprval  47480  prprval  47515  isisubgr  47862  isgrim  47882  uhgrimisgrgric  47931  grtri  47939  isgrlim  47981  usgrexmpl2nb0  48022  usgrexmpl2nb1  48023  usgrexmpl2nb3  48025  upwlksfval  48123  isupwlkg  48125  intopval  48190  clintopval  48192  assintopval  48193  rngcvalALTV  48253  ringcvalALTV  48277  dmatbas  48392  lincop  48397  lcoop  48400  fdivval  48528  blenval  48560  itcoval  48650  itcoval1  48652  itcoval2  48653  itcoval3  48654  itcovalsucov  48657  lines  48720  spheres  48735  discsnterm  49563  termolmd  49659