Theorem elex 3498

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

Syntax hints:   → wi 4   = wceq 1536  ∃wex 1775   ∈ wcel 2105  Vcvv 3477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479

This theorem is referenced by:  elexi  3500  elexd  3501  prcnel  3504  spcimgfi1OLD  3547  vtoclgf  3568  vtocl2gf  3571  vtocl3gf  3572  vtocl2g  3573  vtocl3g  3574  spcgv  3595  spc3egv  3602  elab4g  3685  elrabf  3690  elrab  3694  elrab2w  3698  class2seteq  3712  mob  3725  sbcex  3800  sbcel1v  3861  sbcabel  3886  csbiebt  3937  eldif  3972  elin  3978  ssv  4019  elun  4162  csbnestgfw  4427  sbcco3gw  4430  csbnestgf  4432  sbcco3g  4435  csbco3g  4436  csbvarg  4439  sbccsb2  4442  elpwb  4612  pwidb  4625  elpr2g  4655  snidb  4665  ifpr  4697  snssg  4787  eldifvsn  4801  preqsnd  4863  elpreqpr  4871  dfopg  4875  eluni  4914  eliun  4999  csbexg  5315  nvel  5321  axpweq  5356  reusv2lem4  5406  elopab  5536  epelg  5589  opelvvg  5729  opeliunxp2  5851  opelres  6005  imasng  6103  elimasni  6111  iniseg  6117  inisegn0  6118  dmmptg  6263  elon2  6396  ordsssuc2  6476  iota2  6551  fnmptf  6704  fnmpt  6708  fvelimab  6980  mpteqb  7034  fvmptt  7035  fvmptf  7036  fvopab5  7048  fvopab6  7049  fprg  7174  eloprabga  7540  eloprabgaOLD  7541  ovmpos  7580  ov2gf  7581  ovmpox  7585  ovmpoga  7586  ovmpt3rab1  7690  brrpssg  7743  sorpssi  7747  unexgOLD  7767  elpwun  7787  ordeleqon  7800  onintrab  7815  sucexg  7824  sucexeloni  7828  ordsucelsuc  7841  onzsl  7866  dmfexALT  7930  elxp5  7945  fabexg  7958  f1oabexg  7962  offval3  8005  releldm2  8066  fnmpo  8092  mpoexg  8099  mptmpoopabbrdOLDOLD  8106  bropfvvvv  8115  fsplitfpar  8141  suppval  8185  opeliunxp2f  8233  brtpos2  8255  undefval  8299  tfr2b  8434  tz7.49  8483  oeordi  8623  relelec  8790  ecdmn0  8792  mapvalg  8874  pmvalg  8875  elpmg  8881  elixp2  8939  mptelixpg  8973  elixpsn  8975  2pwuninel  9170  rex2dom  9279  fival  9449  elfi2  9451  dffi2  9460  elfiun  9467  wemapso2lem  9589  harval  9597  brwdom  9604  fowdom  9608  brwdom2  9610  brwdom3  9619  en2lp  9643  cantnfsuc  9707  rankvalb  9834  rankwflem  9852  rankr1g  9869  r1pwALT  9883  r1rankid  9896  djulcl  9947  djurcl  9948  inlresf  9951  inrresf  9953  djuss  9957  1stinl  9964  2ndinl  9965  1stinr  9966  2ndinr  9967  cardval3  9989  dfac8alem  10066  isacn  10081  numacn  10086  acndom  10088  cardinfima  10134  unialeph  10138  ackbij1lem5  10260  cflm  10287  isf32lem2  10391  isfin1-2  10422  itunifval  10453  numth3  10507  ttukeylem1  10546  cardidg  10585  ondomon  10600  elwina  10723  elina  10724  wuncval  10779  tskmval  10876  eltskm  10880  recmulnq  11001  elnp  11024  elnpi  11025  npomex  11033  elfzp12  13639  seqp1  14053  hashinf  14370  hashxnn0  14374  hashnn0pnf  14377  hashxrcl  14392  prsshashgt1  14445  hashmap  14470  lsw  14598  ccatfval  14607  ccats1alpha  14653  swrdval  14677  pfxval  14707  splval  14785  splcl  14786  revval  14794  reps  14804  s3sndisj  15002  s3iunsndisj  15003  trclfv  15035  relexp0g  15057  relexpsucnnr  15060  relexp1g  15061  limsupcl  15505  limsupval  15506  clim  15526  rlim  15527  hashbcval  17035  isstruct2  17182  setsvalg  17199  setsfun0  17205  setscom  17213  strfvnd  17218  setsid  17241  ressval  17276  ressinbas  17290  restval  17472  pwsval  17532  xpsfrnel2  17610  ismre  17634  oppcval  17757  oppccatf  17774  brssc  17861  rescval  17874  issubc  17885  isfunc  17914  homadm  18093  homacd  18094  uncfval  18290  pltfval  18388  lubfval  18407  glbfval  18420  joinfval  18430  meetfval  18444  p0val  18484  p1val  18485  oduclatb  18564  ipoval  18587  pws0g  18798  frmdval  18876  vrmdfval  18881  efmnd  18895  efmnd2hash  18919  eqgfval  19206  gaid  19329  cntzfval  19350  elsymgbas  19405  symg2hash  19423  pmtrfval  19482  symggen  19502  gexval  19610  lsmfval  19670  pj1fval  19726  frgpval  19790  vrgpfval  19798  dmdprd  20032  dprdw  20044  pws1  20338  pwsmgp  20340  dvdsr  20378  isrngim  20461  isrim0OLD  20497  rgspnval  20628  rnghmsscmap  20646  rhmsscmap  20675  lssset  20948  lspfval  20988  islbs  21092  sraval  21191  zlmval  21543  psgnevpmb  21622  ocvfval  21701  cssval  21717  thlval  21730  dsmmval  21771  dsmmbase  21772  frlmval  21785  uvcfval  21821  islinds  21846  ltbval  22078  evlsval  22127  coe1fval  22222  evls1fval  22338  matval  22430  oftpos  22473  dmatval  22513  scmatval  22525  smadiadetglem2  22693  cpmat  22730  mat2pmatfval  22744  cpm2mfval  22770  decpmatval0  22785  pm2mpval  22816  chpmatfval  22851  basdif0  22975  tgval  22977  eltg  22979  eltg2  22980  neipeltop  23152  ordtval  23212  islocfin  23540  txval  23587  qtopval  23718  isfbas  23852  isfildlem  23880  fmval  23966  fmf  23968  isfcls  24032  alexsubb  24069  tsmsfbas  24151  ustval  24226  elutop  24257  isusp  24285  ispsmet  24329  ismet  24348  isxmet  24349  blfvalps  24408  metustel  24578  tngval  24667  elpi1  25091  rrxval  25434  q1peqb  26209  ig1pval  26229  taylfval  26414  ulmval  26437  elno  27704  elnoOLD  27705  nosupno  27762  noetalem2  27801  oldlim  27939  negsval  28071  elzs12  28435  iscgrg  28534  isismt  28556  legval  28606  ishlg  28624  ishpg  28781  iscgra  28831  isinag  28860  isleag  28869  iseqlg  28889  ttgval  28897  ttgvalOLD  28898  xmstrkgc  28914  cplgr2vpr  29464  vtxdgfval  29499  ewlksfval  29633  wksfval  29641  iswlkg  29645  wwlksnon  29880  wspthsnon  29881  avril1  30491  ispligb  30505  gidval  30540  isvcOLD  30607  0vfval  30634  elunop  31900  rabexgfGS  32526  disjdifprg  32594  disjdifprg2  32595  abfmpunirn  32668  rabfmpunirn  32669  hashgt1  32817  mntoval  32956  tocycval  33110  evpmval  33147  altgnsg  33151  sgnsv  33162  inftmrel  33169  isinftm  33170  resvval  33332  ellpi  33380  idlsrgval  33510  rprmval  33523  dimval  33627  dimvalfi  33628  smatfval  33755  lmatval  33773  ispcmp  33817  qqhval2  33944  rrhval  33958  xrhval  33980  indv  33992  esumc  34031  esumpad  34035  esumpcvgval  34058  ofcfval3  34082  issiga  34092  baselsiga  34095  sigasspw  34096  issgon  34103  isrnsigau  34107  sigagenval  34120  ispisys2  34133  cldssbrsiga  34167  sxval  34170  ismeas  34179  cnmbfm  34244  mbfmcnt  34249  elcarsg  34286  sitmval  34330  eulerpartlemt0  34350  sseqval  34369  sseqmw  34372  sseqp1  34376  orvcval  34438  orvcval4  34441  ballotlemsv  34490  prcinf  35086  satf  35337  satfv1lem  35346  satefv  35398  mrexval  35485  mrsubffval  35491  msubffval  35507  mclsval  35547  eldm3  35740  opelco3  35755  elima4  35756  elfix2  35885  elsingles  35899  fvimage  35912  funpartlem  35923  elaltxp  35956  brcolinear2  36039  ellines  36133  topfneec  36337  topfneec2  36338  fnejoin2  36351  limsucncmpi  36427  findabrcl  36436  weiunse  36450  bj-ififc  36564  elelb  36879  bj-pwvrelb  36880  bj-sngltag  36965  bj-xtagex  36971  bj-elsnb  37043  bj-epelg  37050  bj-evalval  37057  bj-ismoore  37087  bj-ideqg1  37146  bj-ideqg1ALT  37147  bj-elid6  37152  bj-diagval  37156  bj-eldiag2  37159  bj-isrvec  37276  finxpreclem1  37371  finxpreclem3  37375  elghomlem2OLD  37872  isrngo  37883  isdivrngo  37936  br1cnvres  38250  riotasv2d  38938  riotasv3d  38941  lshpset  38959  lsatset  38971  lcvfbr  39001  lflset  39040  lkrfval  39068  lkrval2  39071  islshpkrN  39101  ldualset  39106  cmtfvalN  39191  cvrfval  39249  pats  39266  llnset  39487  lplnset  39511  lvolset  39554  lineset  39720  pointsetN  39723  psubspset  39726  pmapfval  39738  paddfval  39779  pclfvalN  39871  polfvalN  39886  psubclsetN  39918  watfvalN  39974  lhpset  39977  lautset  40064  pautsetN  40080  ldilfset  40090  ltrnfset  40099  dilfsetN  40134  trnfsetN  40137  trlfset  40142  tgrpfset  40726  tendofset  40740  erngfset  40781  erngfset-rN  40789  dvafset  40986  diaffval  41012  dvhfset  41062  docaffvalN  41103  djaffvalN  41115  dibffval  41122  dicffval  41156  dihffval  41212  dochffval  41331  djhffval  41378  lpolsetN  41464  lcdfval  41570  mapdffval  41608  hvmapffval  41740  hdmap1ffval  41777  hdmapffval  41808  hgmapffval  41867  hlhilset  41916  elrfi  42681  nacsfix  42699  mapfzcons2  42706  sbc2rexgOLD  42775  sbc4rexgOLD  42777  setindtrs  43013  wepwso  43031  hbtlem1  43111  hbtlem7  43113  mendval  43167  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  44461  subrval  44462  mulvval  44463  elixpconstg  45028  mptfnd  45185  upbdrech  45255  climf  45577  climf2  45621  liminfval  45714  dvcosre  45867  itgsinexplem1  45909  itgsubsticclem  45930  dmvolss  45940  stoweidlem26  45981  stoweidlem35  45990  stirlinglem14  46042  fourierdlem42  46104  fourierdlem81  46142  fourierdlem89  46150  fourierdlem91  46152  salgenval  46276  elsprel  47399  sprval  47403  prprval  47438  isisubgr  47785  isgrim  47805  uhgrimisgrgric  47836  grtri  47844  isgrlim  47884  usgrexmpl2nb0  47925  usgrexmpl2nb1  47926  usgrexmpl2nb3  47928  upwlksfval  47978  isupwlkg  47980  intopval  48045  clintopval  48047  assintopval  48048  rngcvalALTV  48108  ringcvalALTV  48132  dmatbas  48248  lincop  48253  lcoop  48256  fdivval  48388  blenval  48420  itcoval  48510  itcoval1  48512  itcoval2  48513  itcoval3  48514  itcovalsucov  48517  lines  48580  spheres  48595