Theorem elex 3472

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ∃wex 1812   ∈ wcel 2145  Vcvv 3451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453

This theorem is used by:  elexi  3473  elexd  3474  prcnel  3476  vtoclgf  3530  vtocl2gf  3532  vtocl3gf  3533  vtocl2g  3534  vtocl3g  3535  spcgv  3551  spc3egv  3558  elab4g  3637  elrabf  3642  elrab  3645  elrab2w  3650  class2seteq  3662  mob  3675  sbcex  3749  sbcel1v  3804  sbcabel  3825  csbiebt  3876  eldif  3909  elin  3915  ssv  3955  elun  4100  csbnestgfw  4380  sbcco3gw  4383  csbnestgf  4385  sbcco3g  4388  csbco3g  4389  csbvarg  4392  sbccsb2  4395  elpwb  4565  pwidg  4577  pwidb  4579  elpr2g  4610  snidb  4622  ifpr  4654  snssg  4744  eldifvsn  4760  preqsnd  4819  elpreqpr  4827  dfopg  4831  eluni  4870  eliun  4955  csbexg  5264  nvelOLD  5276  axpweq  5312  reusv2lem4  5363  elopab  5501  epelg  5552  opelvvg  5692  opeliunxp2  5815  opelres  5976  imasng  6082  elimasni  6089  iniseg  6095  inisegn0  6096  dmmptg  6243  elon2  6373  ordsssuc2  6456  iota2  6527  fnmptf  6675  fnmpt  6679  fvelimab  6957  mpteqb  7013  fvmptt  7014  fvmptf  7015  fvopab5  7027  fvopab6  7028  fprg  7159  eloprabga  7529  ovmpos  7568  ov2gf  7569  ovmpox  7573  ovmpoga  7574  ovmpt3rab1  7679  brrpssg  7741  sorpssi  7745  elpwun  7783  ordeleqon  7796  onintrab  7810  sucexg  7819  sucexeloni  7823  ordsucelsuc  7833  onzsl  7857  dmfexALT  7920  elxp5  7935  fabexg  7950  f1oabexg  7953  offval3  7994  releldm2  8054  fnmpo  8080  mpoexg  8089  bropfvvvv  8103  fsplitfpar  8129  suppval  8179  opeliunxp2f  8227  brtpos2  8249  undefval  8294  tfr2b  8404  tz7.49  8455  oeordi  8596  relelec  8765  ecdmn0  8770  mapvalg  8856  pmvalg  8857  elpmg  8863  elixp2  8929  mptelixpg  8963  elixpsn  8965  2pwuninel  9151  ordfin  9231  rex2dom  9244  fival  9404  elfi2  9406  dffi2  9415  elfiun  9422  wemapso2lem  9546  harval  9554  brwdom  9561  fowdom  9565  brwdom2  9567  brwdom3  9576  en2lp  9607  cantnfsuc  9671  rankvalb  9805  rankwflem  9824  rankr1g  9844  r1pwALT  9860  r1rankid  9875  djulcl  9991  djurcl  9992  inlresf  9995  inrresf  9997  djuss  10001  1stinl  10008  2ndinl  10009  1stinr  10010  2ndinr  10011  cardval3  10033  dfac8alem  10108  isacn  10123  numacn  10128  acndom  10130  cardinfima  10176  unialeph  10180  ackbij1lem5  10301  cflm  10327  isf32lem2  10432  isfin1-2  10463  itunifval  10494  numth3  10548  ttukeylem1  10587  imadomnum  10614  cardidg  10632  ondomon  10647  elwina  10771  elina  10772  wuncval  10827  tskmval  10924  eltskm  10928  recmulnq  11049  elnp  11072  elnpi  11073  npomex  11081  indv  12322  elfzp12  13737  seqp1  14159  hashinf  14479  hashxnn0  14483  hashnn0pnf  14486  hashxrcl  14501  prsshashgt1  14555  hashmap  14580  lsw  14709  ccatfval  14718  ccats1alpha  14767  swrdval  14791  pfxval  14823  splval  14900  splcl  14901  revval  14909  reps  14921  s3sndisj  15120  s3iunsndisj  15121  trclfv  15153  relexp0g  15175  relexpsucnnr  15178  relexp1g  15179  limsupcl  15640  limsupval  15641  clim  15661  rlim  15662  hashbcval  17180  isstruct2  17327  setsvalg  17344  setsfun0  17350  setscom  17358  strfvnd  17363  setsid  17385  ressval  17411  ressinbas  17423  restval  17597  pwsval  17657  xpsfrnel2  17736  ismre  17760  oppcval  17887  oppccatf  17902  brssc  17989  rescval  18002  issubc  18010  isfunc  18039  homadm  18215  homacd  18216  uncfval  18408  pltfval  18503  lubfval  18522  glbfval  18535  joinfval  18545  meetfval  18559  p0val  18599  p1val  18600  oduclatb  18681  ipoval  18704  pws0g  18967  frmdval  19047  vrmdfval  19052  efmnd  19066  efmnd2hash  19090  eqgfval  19388  gaid  19513  cntzfval  19534  elsymgbas  19588  symg2hash  19606  pmtrfval  19664  symggen  19684  gexval  19792  lsmfval  19852  pj1fval  19908  frgpval  19972  vrgpfval  19980  dmdprd  20214  dprdw  20226  pws1  20554  pwsmgp  20556  dvdsr  20592  isrngim  20675  rgspnval  20864  rnghmsscmap  20882  rhmsscmap  20911  lssset  21208  lspfval  21248  islbs  21351  sraval  21450  zlmval  21821  psgnevpmb  21893  ocvfval  21972  cssval  21988  thlval  22001  dsmmval  22040  dsmmbase  22041  frlmval  22054  uvcfval  22090  islinds  22115  ltbval  22352  evlsval  22395  coe1fval  22523  evls1fval  22637  matval  22726  oftpos  22767  dmatval  22807  scmatval  22819  smadiadetglem2  22987  cpmat  23027  mat2pmatfval  23041  cpm2mfval  23067  decpmatval0  23082  pm2mpval  23113  chpmatfval  23148  basdif0  23271  tgval  23273  eltg  23275  eltg2  23276  neipeltop  23447  ordtval  23507  islocfin  23836  txval  23883  qtopval  24014  isfbas  24148  isfildlem  24176  fmval  24262  fmf  24264  isfcls  24328  alexsubb  24365  tsmsfbas  24447  ustval  24522  elutop  24552  isusp  24580  ispsmet  24623  ismet  24642  isxmet  24643  blfvalps  24702  metustel  24869  tngval  24958  elpi1  25366  rrxval  25708  q1peqb  26474  ig1pval  26494  taylfval  26686  ulmval  26707  elno  28003  nosupno  28060  noetalem2  28099  nulslts  28161  oldlim  28273  negsval  28411  elz12s  28858  iscgrg  28975  isismt  28997  legval  29047  ishlg2  29065  ishlg  29068  ishpg  29237  iscgra  29316  isinag  29357  isleag  29366  angmgmval  29394  iseqlg  29412  ttgval  29452  xmstrkgc  29463  cplgr2vpr  30014  vtxdgfval  30048  ewlksfval  30182  wksfval  30190  iswlkg  30194  wwlksnon  30440  wspthsnon  30441  avril1  31064  ispligb  31079  gidval  31114  isvcOLD  31181  0vfval  31208  elunop  32474  rabexgfGS  33095  disjdifprg  33169  disjdifprg2  33170  abfmpunirn  33246  rabfmpunirn  33247  hashgt1  33400  mntoval  33543  tocycval  33669  evpmval  33706  altgnsg  33710  sgnsv  33721  inftmrel  33741  isinftm  33742  resvval  33890  ellpi  33928  idlsrgval  34035  rprmval  34048  dimval  34233  dimvalfi  34234  smatfval  34427  lmatval  34445  ispcmp  34489  qqhval2  34614  rrhval  34628  xrhval  34650  esumc  34683  esumpad  34687  esumpcvgval  34710  ofcfval3  34734  issiga  34744  baselsiga  34747  sigasspw  34748  issgon  34755  isrnsigau  34759  sigagenval  34773  ispisys2  34786  cldssbrsiga  34820  sxval  34823  ismeas  34832  cnmbfm  34895  mbfmcnt  34900  elcarsg  34937  sitmval  34981  eulerpartlemt0  35001  sseqval  35020  sseqmw  35023  sseqp1  35027  orvcval  35090  orvcval4  35093  ballotlemsv  35142  acnum  35755  prcinf  35781  satf  36118  satfv1lem  36127  satefv  36179  mrexval  36266  mrsubffval  36272  msubffval  36288  mclsval  36328  eldm3  36526  opelco3  36539  elima4  36540  elfix2  36666  elsingles  36680  fvimage  36693  funpartlem  36706  elaltxp  36740  brcolinear2  36823  ellines  36917  topfneec  37143  topfneec2  37144  fnejoin2  37157  limsucncmpi  37233  findabrcl  37242  weiunse  37256  ttcwf2  37313  bj-ififc  37452  elelb  37809  bj-pwvrelb  37810  bj-sngltag  37896  bj-xtagex  37902  bj-elsnb  37976  bj-epelg  37983  bj-evalval  37996  bj-ismoore  38026  bj-ideqg1  38085  bj-ideqg1ALT  38086  bj-elid6  38091  bj-diagval  38095  bj-eldiag2  38098  bj-isrvec  38215  finxpreclem1  38312  finxpreclem3  38316  elghomlem2OLD  38820  isrngo  38831  isdivrngo  38884  br1cnvres  39206  riotasv2d  40014  riotasv3d  40017  lshpset  40035  lsatset  40047  lcvfbr  40077  lflset  40116  lkrfval  40144  lkrval2  40147  islshpkrN  40177  ldualset  40182  cmtfvalN  40267  cvrfval  40325  pats  40342  llnset  40562  lplnset  40586  lvolset  40629  lineset  40795  pointsetN  40798  psubspset  40801  pmapfval  40813  paddfval  40854  pclfvalN  40946  polfvalN  40961  psubclsetN  40993  watfvalN  41049  lhpset  41052  lautset  41139  pautsetN  41155  ldilfset  41165  ltrnfset  41174  dilfsetN  41209  trnfsetN  41212  trlfset  41217  tgrpfset  41801  tendofset  41815  erngfset  41856  erngfset-rN  41864  dvafset  42061  diaffval  42087  dvhfset  42137  docaffvalN  42178  djaffvalN  42190  dibffval  42197  dicffval  42231  dihffval  42287  dochffval  42406  djhffval  42453  lpolsetN  42539  lcdfval  42645  mapdffval  42683  hvmapffval  42815  hdmap1ffval  42852  hdmapffval  42883  hgmapffval  42942  hlhilset  42991  elrfi  43704  nacsfix  43722  mapfzcons2  43729  setindtrs  44031  wepwso  44049  hbtlem1  44124  hbtlem7  44126  mendval  44180  oaltublim  44291  omord2lim  44301  cnvtrucl0  44623  eliunov2  44678  iunrelexpmin1  44707  iunrelexpmin2  44711  trclfvcom  44722  cnvtrclfv  44723  trclimalb2  44725  trclfvdecomr  44727  gneispacef2  45135  gneispacern2  45138  gneispace0nelrn  45139  addrval  45447  subrval  45448  mulvval  45449  orbitclmpt  45947  elixpconstg  46103  mptfnd  46253  upbdrech  46320  climf  46633  climf2  46675  liminfval  46768  dvcosre  46921  itgsinexplem1  46963  itgsubsticclem  46984  dmvolss  46994  stoweidlem26  47035  stoweidlem35  47044  stirlinglem14  47096  fourierdlem42  47158  fourierdlem81  47196  fourierdlem89  47204  fourierdlem91  47206  salgenval  47330  elsprel  48556  sprval  48560  prprval  48595  isisubgr  48959  isgrim  48979  uhgrimisgrgric  49028  grtri  49037  isgrlim  49079  usgrexmpl2nb0  49128  usgrexmpl2nb1  49129  usgrexmpl2nb3  49131  upwlksfval  49232  isupwlkg  49234  intopval  49298  clintopval  49300  assintopval  49301  rngcvalALTV  49361  ringcvalALTV  49385  dmatbas  49514  lincop  49519  lcoop  49522  fdivval  49650  blenval  49682  itcoval  49772  itcoval1  49774  itcoval2  49775  itcoval3  49776  itcovalsucov  49779  lines  49842  spheres  49857  discsnterm  50681  termolmd  50777