Theorem elex 3501

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

Syntax hints:   → wi 4   = wceq 1540  ∃wex 1779   ∈ wcel 2108  Vcvv 3480

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482

This theorem is referenced by:  elexi  3503  elexd  3504  prcnel  3507  spcimgfi1OLD  3548  vtoclgf  3569  vtocl2gf  3572  vtocl3gf  3573  vtocl2g  3574  vtocl3g  3575  spcgv  3596  spc3egv  3603  elab4g  3683  elrabf  3688  elrab  3692  elrab2w  3696  class2seteq  3710  mob  3723  sbcex  3798  sbcel1v  3856  sbcabel  3878  csbiebt  3928  eldif  3961  elin  3967  ssv  4008  elun  4153  csbnestgfw  4422  sbcco3gw  4425  csbnestgf  4427  sbcco3g  4430  csbco3g  4431  csbvarg  4434  sbccsb2  4437  elpwb  4608  pwidb  4621  elpr2g  4651  snidb  4661  ifpr  4693  snssg  4783  eldifvsn  4797  preqsnd  4859  elpreqpr  4867  dfopg  4871  eluni  4910  eliun  4995  csbexg  5310  nvel  5316  axpweq  5351  reusv2lem4  5401  elopab  5532  epelg  5585  opelvvg  5726  opeliunxp2  5849  opelres  6003  imasng  6102  elimasni  6109  iniseg  6115  inisegn0  6116  dmmptg  6262  elon2  6395  ordsssuc2  6475  iota2  6550  fnmptf  6704  fnmpt  6708  fvelimab  6981  mpteqb  7035  fvmptt  7036  fvmptf  7037  fvopab5  7049  fvopab6  7050  fprg  7175  eloprabga  7542  ovmpos  7581  ov2gf  7582  ovmpox  7586  ovmpoga  7587  ovmpt3rab1  7691  brrpssg  7745  sorpssi  7749  unexgOLD  7769  elpwun  7789  ordeleqon  7802  onintrab  7816  sucexg  7825  sucexeloni  7829  ordsucelsuc  7842  onzsl  7867  dmfexALT  7930  elxp5  7945  fabexg  7960  f1oabexg  7964  offval3  8007  releldm2  8068  fnmpo  8094  mpoexg  8101  mptmpoopabbrdOLDOLD  8108  bropfvvvv  8117  fsplitfpar  8143  suppval  8187  opeliunxp2f  8235  brtpos2  8257  undefval  8301  tfr2b  8436  tz7.49  8485  oeordi  8625  relelec  8792  ecdmn0  8794  mapvalg  8876  pmvalg  8877  elpmg  8883  elixp2  8941  mptelixpg  8975  elixpsn  8977  2pwuninel  9172  rex2dom  9282  fival  9452  elfi2  9454  dffi2  9463  elfiun  9470  wemapso2lem  9592  harval  9600  brwdom  9607  fowdom  9611  brwdom2  9613  brwdom3  9622  en2lp  9646  cantnfsuc  9710  rankvalb  9837  rankwflem  9855  rankr1g  9872  r1pwALT  9886  r1rankid  9899  djulcl  9950  djurcl  9951  inlresf  9954  inrresf  9956  djuss  9960  1stinl  9967  2ndinl  9968  1stinr  9969  2ndinr  9970  cardval3  9992  dfac8alem  10069  isacn  10084  numacn  10089  acndom  10091  cardinfima  10137  unialeph  10141  ackbij1lem5  10263  cflm  10290  isf32lem2  10394  isfin1-2  10425  itunifval  10456  numth3  10510  ttukeylem1  10549  cardidg  10588  ondomon  10603  elwina  10726  elina  10727  wuncval  10782  tskmval  10879  eltskm  10883  recmulnq  11004  elnp  11027  elnpi  11028  npomex  11036  elfzp12  13643  seqp1  14057  hashinf  14374  hashxnn0  14378  hashnn0pnf  14381  hashxrcl  14396  prsshashgt1  14449  hashmap  14474  lsw  14602  ccatfval  14611  ccats1alpha  14657  swrdval  14681  pfxval  14711  splval  14789  splcl  14790  revval  14798  reps  14808  s3sndisj  15006  s3iunsndisj  15007  trclfv  15039  relexp0g  15061  relexpsucnnr  15064  relexp1g  15065  limsupcl  15509  limsupval  15510  clim  15530  rlim  15531  hashbcval  17040  isstruct2  17186  setsvalg  17203  setsfun0  17209  setscom  17217  strfvnd  17222  setsid  17244  ressval  17277  ressinbas  17291  restval  17471  pwsval  17531  xpsfrnel2  17609  ismre  17633  oppcval  17756  oppccatf  17771  brssc  17858  rescval  17871  issubc  17880  isfunc  17909  homadm  18085  homacd  18086  uncfval  18279  pltfval  18376  lubfval  18395  glbfval  18408  joinfval  18418  meetfval  18432  p0val  18472  p1val  18473  oduclatb  18552  ipoval  18575  pws0g  18786  frmdval  18864  vrmdfval  18869  efmnd  18883  efmnd2hash  18907  eqgfval  19194  gaid  19317  cntzfval  19338  elsymgbas  19391  symg2hash  19409  pmtrfval  19468  symggen  19488  gexval  19596  lsmfval  19656  pj1fval  19712  frgpval  19776  vrgpfval  19784  dmdprd  20018  dprdw  20030  pws1  20322  pwsmgp  20324  dvdsr  20362  isrngim  20445  isrim0OLD  20481  rgspnval  20612  rnghmsscmap  20630  rhmsscmap  20659  lssset  20931  lspfval  20971  islbs  21075  sraval  21174  zlmval  21526  psgnevpmb  21605  ocvfval  21684  cssval  21700  thlval  21713  dsmmval  21754  dsmmbase  21755  frlmval  21768  uvcfval  21804  islinds  21829  ltbval  22061  evlsval  22110  coe1fval  22207  evls1fval  22323  matval  22415  oftpos  22458  dmatval  22498  scmatval  22510  smadiadetglem2  22678  cpmat  22715  mat2pmatfval  22729  cpm2mfval  22755  decpmatval0  22770  pm2mpval  22801  chpmatfval  22836  basdif0  22960  tgval  22962  eltg  22964  eltg2  22965  neipeltop  23137  ordtval  23197  islocfin  23525  txval  23572  qtopval  23703  isfbas  23837  isfildlem  23865  fmval  23951  fmf  23953  isfcls  24017  alexsubb  24054  tsmsfbas  24136  ustval  24211  elutop  24242  isusp  24270  ispsmet  24314  ismet  24333  isxmet  24334  blfvalps  24393  metustel  24563  tngval  24652  elpi1  25078  rrxval  25421  q1peqb  26195  ig1pval  26215  taylfval  26400  ulmval  26423  elno  27690  elnoOLD  27691  nosupno  27748  noetalem2  27787  oldlim  27925  negsval  28057  elzs12  28421  iscgrg  28520  isismt  28542  legval  28592  ishlg  28610  ishpg  28767  iscgra  28817  isinag  28846  isleag  28855  iseqlg  28875  ttgval  28883  ttgvalOLD  28884  xmstrkgc  28900  cplgr2vpr  29450  vtxdgfval  29485  ewlksfval  29619  wksfval  29627  iswlkg  29631  wwlksnon  29871  wspthsnon  29872  avril1  30482  ispligb  30496  gidval  30531  isvcOLD  30598  0vfval  30625  elunop  31891  rabexgfGS  32518  disjdifprg  32588  disjdifprg2  32589  abfmpunirn  32662  rabfmpunirn  32663  hashgt1  32812  indv  32837  mntoval  32972  tocycval  33128  evpmval  33165  altgnsg  33169  sgnsv  33180  inftmrel  33187  isinftm  33188  resvval  33353  ellpi  33401  idlsrgval  33531  rprmval  33544  dimval  33651  dimvalfi  33652  smatfval  33794  lmatval  33812  ispcmp  33856  qqhval2  33983  rrhval  33997  xrhval  34019  esumc  34052  esumpad  34056  esumpcvgval  34079  ofcfval3  34103  issiga  34113  baselsiga  34116  sigasspw  34117  issgon  34124  isrnsigau  34128  sigagenval  34141  ispisys2  34154  cldssbrsiga  34188  sxval  34191  ismeas  34200  cnmbfm  34265  mbfmcnt  34270  elcarsg  34307  sitmval  34351  eulerpartlemt0  34371  sseqval  34390  sseqmw  34393  sseqp1  34397  orvcval  34460  orvcval4  34463  ballotlemsv  34512  prcinf  35108  satf  35358  satfv1lem  35367  satefv  35419  mrexval  35506  mrsubffval  35512  msubffval  35528  mclsval  35568  eldm3  35761  opelco3  35775  elima4  35776  elfix2  35905  elsingles  35919  fvimage  35932  funpartlem  35943  elaltxp  35976  brcolinear2  36059  ellines  36153  topfneec  36356  topfneec2  36357  fnejoin2  36370  limsucncmpi  36446  findabrcl  36455  weiunse  36469  bj-ififc  36583  elelb  36898  bj-pwvrelb  36899  bj-sngltag  36984  bj-xtagex  36990  bj-elsnb  37062  bj-epelg  37069  bj-evalval  37076  bj-ismoore  37106  bj-ideqg1  37165  bj-ideqg1ALT  37166  bj-elid6  37171  bj-diagval  37175  bj-eldiag2  37178  bj-isrvec  37295  finxpreclem1  37390  finxpreclem3  37394  elghomlem2OLD  37893  isrngo  37904  isdivrngo  37957  br1cnvres  38270  riotasv2d  38958  riotasv3d  38961  lshpset  38979  lsatset  38991  lcvfbr  39021  lflset  39060  lkrfval  39088  lkrval2  39091  islshpkrN  39121  ldualset  39126  cmtfvalN  39211  cvrfval  39269  pats  39286  llnset  39507  lplnset  39531  lvolset  39574  lineset  39740  pointsetN  39743  psubspset  39746  pmapfval  39758  paddfval  39799  pclfvalN  39891  polfvalN  39906  psubclsetN  39938  watfvalN  39994  lhpset  39997  lautset  40084  pautsetN  40100  ldilfset  40110  ltrnfset  40119  dilfsetN  40154  trnfsetN  40157  trlfset  40162  tgrpfset  40746  tendofset  40760  erngfset  40801  erngfset-rN  40809  dvafset  41006  diaffval  41032  dvhfset  41082  docaffvalN  41123  djaffvalN  41135  dibffval  41142  dicffval  41176  dihffval  41232  dochffval  41351  djhffval  41398  lpolsetN  41484  lcdfval  41590  mapdffval  41628  hvmapffval  41760  hdmap1ffval  41797  hdmapffval  41828  hgmapffval  41887  hlhilset  41936  elrfi  42705  nacsfix  42723  mapfzcons2  42730  sbc2rexgOLD  42799  sbc4rexgOLD  42801  setindtrs  43037  wepwso  43055  hbtlem1  43135  hbtlem7  43137  mendval  43191  oaltublim  43303  omord2lim  43313  cnvtrucl0  43637  eliunov2  43692  iunrelexpmin1  43721  iunrelexpmin2  43725  trclfvcom  43736  cnvtrclfv  43737  trclimalb2  43739  trclfvdecomr  43741  gneispacef2  44149  gneispacern2  44152  gneispace0nelrn  44153  addrval  44485  subrval  44486  mulvval  44487  elixpconstg  45094  mptfnd  45248  upbdrech  45317  climf  45637  climf2  45681  liminfval  45774  dvcosre  45927  itgsinexplem1  45969  itgsubsticclem  45990  dmvolss  46000  stoweidlem26  46041  stoweidlem35  46050  stirlinglem14  46102  fourierdlem42  46164  fourierdlem81  46202  fourierdlem89  46210  fourierdlem91  46212  salgenval  46336  elsprel  47462  sprval  47466  prprval  47501  isisubgr  47848  isgrim  47868  uhgrimisgrgric  47899  grtri  47907  isgrlim  47949  usgrexmpl2nb0  47990  usgrexmpl2nb1  47991  usgrexmpl2nb3  47993  upwlksfval  48051  isupwlkg  48053  intopval  48118  clintopval  48120  assintopval  48121  rngcvalALTV  48181  ringcvalALTV  48205  dmatbas  48320  lincop  48325  lcoop  48328  fdivval  48460  blenval  48492  itcoval  48582  itcoval1  48584  itcoval2  48585  itcoval3  48586  itcovalsucov  48589  lines  48652  spheres  48667