Theorem elex 3471

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  elexi  3472  elexd  3473  prcnel  3475  vtoclgf  3529  vtocl2gf  3531  vtocl3gf  3532  vtocl2g  3533  vtocl3g  3534  spcgv  3550  spc3egv  3557  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  5267  nvelOLD  5279  axpweq  5315  reusv2lem4  5366  elopab  5505  epelg  5556  opelvvg  5696  opeliunxp2  5818  opelres  5978  imasng  6080  elimasni  6087  iniseg  6093  inisegn0  6094  dmmptg  6238  elon2  6368  ordsssuc2  6451  iota2  6522  fnmptf  6669  fnmpt  6673  fvelimab  6951  mpteqb  7007  fvmptt  7008  fvmptf  7009  fvopab5  7021  fvopab6  7022  fprg  7153  eloprabga  7523  ovmpos  7562  ov2gf  7563  ovmpox  7567  ovmpoga  7568  ovmpt3rab1  7673  brrpssg  7727  sorpssi  7731  elpwun  7769  ordeleqon  7782  onintrab  7796  sucexg  7805  sucexeloni  7809  ordsucelsuc  7819  onzsl  7843  dmfexALT  7906  elxp5  7921  fabexg  7936  f1oabexg  7939  offval3  7980  releldm2  8041  fnmpo  8067  mpoexg  8076  bropfvvvv  8090  fsplitfpar  8116  suppval  8161  opeliunxp2f  8209  brtpos2  8231  undefval  8276  tfr2b  8386  tz7.49  8437  oeordi  8578  relelec  8747  ecdmn0  8752  mapvalg  8838  pmvalg  8839  elpmg  8845  elixp2  8911  mptelixpg  8945  elixpsn  8947  2pwuninel  9133  ordfin  9213  rex2dom  9226  fival  9385  elfi2  9387  dffi2  9396  elfiun  9403  wemapso2lem  9527  harval  9535  brwdom  9542  fowdom  9546  brwdom2  9548  brwdom3  9557  en2lp  9588  cantnfsuc  9652  rankvalb  9782  rankwflem  9800  rankr1g  9817  r1pwALT  9831  r1rankid  9844  djulcl  9918  djurcl  9919  inlresf  9922  inrresf  9924  djuss  9928  1stinl  9935  2ndinl  9936  1stinr  9937  2ndinr  9938  cardval3  9960  dfac8alem  10035  isacn  10050  numacn  10055  acndom  10057  cardinfima  10103  unialeph  10107  ackbij1lem5  10228  cflm  10254  isf32lem2  10359  isfin1-2  10390  itunifval  10421  numth3  10475  ttukeylem1  10514  imadomnum  10541  cardidg  10559  ondomon  10574  elwina  10698  elina  10699  wuncval  10754  tskmval  10851  eltskm  10855  recmulnq  10976  elnp  10999  elnpi  11000  npomex  11008  indv  12247  elfzp12  13661  seqp1  14083  hashinf  14402  hashxnn0  14406  hashnn0pnf  14409  hashxrcl  14424  prsshashgt1  14478  hashmap  14503  lsw  14632  ccatfval  14641  ccats1alpha  14690  swrdval  14714  pfxval  14746  splval  14823  splcl  14824  revval  14832  reps  14844  s3sndisj  15043  s3iunsndisj  15044  trclfv  15076  relexp0g  15098  relexpsucnnr  15101  relexp1g  15102  limsupcl  15563  limsupval  15564  clim  15584  rlim  15585  hashbcval  17097  isstruct2  17244  setsvalg  17261  setsfun0  17267  setscom  17275  strfvnd  17280  setsid  17302  ressval  17328  ressinbas  17340  restval  17514  pwsval  17574  xpsfrnel2  17653  ismre  17677  oppcval  17804  oppccatf  17819  brssc  17906  rescval  17919  issubc  17927  isfunc  17956  homadm  18132  homacd  18133  uncfval  18325  pltfval  18420  lubfval  18439  glbfval  18452  joinfval  18462  meetfval  18476  p0val  18516  p1val  18517  oduclatb  18598  ipoval  18621  pws0g  18883  frmdval  18963  vrmdfval  18968  efmnd  18982  efmnd2hash  19006  eqgfval  19304  gaid  19429  cntzfval  19450  elsymgbas  19504  symg2hash  19522  pmtrfval  19580  symggen  19600  gexval  19708  lsmfval  19768  pj1fval  19824  frgpval  19888  vrgpfval  19896  dmdprd  20130  dprdw  20142  pws1  20468  pwsmgp  20470  dvdsr  20506  isrngim  20589  rgspnval  20777  rnghmsscmap  20795  rhmsscmap  20824  lssset  21120  lspfval  21160  islbs  21263  sraval  21362  zlmval  21731  psgnevpmb  21803  ocvfval  21882  cssval  21898  thlval  21911  dsmmval  21950  dsmmbase  21951  frlmval  21964  uvcfval  22000  islinds  22025  ltbval  22262  evlsval  22305  coe1fval  22433  evls1fval  22547  matval  22636  oftpos  22677  dmatval  22717  scmatval  22729  smadiadetglem2  22897  cpmat  22937  mat2pmatfval  22951  cpm2mfval  22977  decpmatval0  22992  pm2mpval  23023  chpmatfval  23058  basdif0  23181  tgval  23183  eltg  23185  eltg2  23186  neipeltop  23357  ordtval  23417  islocfin  23746  txval  23793  qtopval  23924  isfbas  24058  isfildlem  24086  fmval  24172  fmf  24174  isfcls  24238  alexsubb  24275  tsmsfbas  24357  ustval  24432  elutop  24462  isusp  24490  ispsmet  24533  ismet  24552  isxmet  24553  blfvalps  24612  metustel  24779  tngval  24868  elpi1  25276  rrxval  25618  q1peqb  26384  ig1pval  26404  taylfval  26598  ulmval  26619  elno  27885  nosupno  27942  noetalem2  27981  nulslts  28043  oldlim  28155  negsval  28293  elz12s  28740  iscgrg  28857  isismt  28879  legval  28929  ishlg2  28947  ishlg  28950  ishpg  29119  iscgra  29198  isinag  29239  isleag  29248  angmgmval  29276  iseqlg  29294  ttgval  29334  xmstrkgc  29345  cplgr2vpr  29896  vtxdgfval  29930  ewlksfval  30064  wksfval  30072  iswlkg  30076  wwlksnon  30322  wspthsnon  30323  avril1  30946  ispligb  30961  gidval  30996  isvcOLD  31063  0vfval  31090  elunop  32356  rabexgfGS  32977  disjdifprg  33051  disjdifprg2  33052  abfmpunirn  33128  rabfmpunirn  33129  hashgt1  33282  mntoval  33425  tocycval  33551  evpmval  33588  altgnsg  33592  sgnsv  33603  inftmrel  33623  isinftm  33624  resvval  33772  ellpi  33810  idlsrgval  33916  rprmval  33929  dimval  34114  dimvalfi  34115  smatfval  34308  lmatval  34326  ispcmp  34370  qqhval2  34495  rrhval  34509  xrhval  34531  esumc  34564  esumpad  34568  esumpcvgval  34591  ofcfval3  34615  issiga  34625  baselsiga  34628  sigasspw  34629  issgon  34636  isrnsigau  34640  sigagenval  34654  ispisys2  34667  cldssbrsiga  34701  sxval  34704  ismeas  34713  cnmbfm  34777  mbfmcnt  34782  elcarsg  34819  sitmval  34863  eulerpartlemt0  34883  sseqval  34902  sseqmw  34905  sseqp1  34909  orvcval  34972  orvcval4  34975  ballotlemsv  35024  acnum  35641  prcinf  35642  satf  35935  satfv1lem  35944  satefv  35996  mrexval  36083  mrsubffval  36089  msubffval  36105  mclsval  36145  eldm3  36343  opelco3  36357  elima4  36358  elfix2  36484  elsingles  36498  fvimage  36511  funpartlem  36524  elaltxp  36558  brcolinear2  36641  ellines  36735  topfneec  36977  topfneec2  36978  fnejoin2  36991  limsucncmpi  37067  findabrcl  37076  weiunse  37090  ttcwf2  37147  bj-ififc  37286  elelb  37643  bj-pwvrelb  37644  bj-sngltag  37730  bj-xtagex  37736  bj-elsnb  37808  bj-epelg  37815  bj-evalval  37828  bj-ismoore  37858  bj-ideqg1  37919  bj-ideqg1ALT  37920  bj-elid6  37925  bj-diagval  37929  bj-eldiag2  37932  bj-isrvec  38049  finxpreclem1  38146  finxpreclem3  38150  elghomlem2OLD  38639  isrngo  38650  isdivrngo  38703  br1cnvres  39025  riotasv2d  39833  riotasv3d  39836  lshpset  39854  lsatset  39866  lcvfbr  39896  lflset  39935  lkrfval  39963  lkrval2  39966  islshpkrN  39996  ldualset  40001  cmtfvalN  40086  cvrfval  40144  pats  40161  llnset  40381  lplnset  40405  lvolset  40448  lineset  40614  pointsetN  40617  psubspset  40620  pmapfval  40632  paddfval  40673  pclfvalN  40765  polfvalN  40780  psubclsetN  40812  watfvalN  40868  lhpset  40871  lautset  40958  pautsetN  40974  ldilfset  40984  ltrnfset  40993  dilfsetN  41028  trnfsetN  41031  trlfset  41036  tgrpfset  41620  tendofset  41634  erngfset  41675  erngfset-rN  41683  dvafset  41880  diaffval  41906  dvhfset  41956  docaffvalN  41997  djaffvalN  42009  dibffval  42016  dicffval  42050  dihffval  42106  dochffval  42225  djhffval  42272  lpolsetN  42358  lcdfval  42464  mapdffval  42502  hvmapffval  42634  hdmap1ffval  42671  hdmapffval  42702  hgmapffval  42761  hlhilset  42810  elrfi  43542  nacsfix  43560  mapfzcons2  43567  setindtrs  43869  wepwso  43887  hbtlem1  43967  hbtlem7  43969  mendval  44023  oaltublim  44134  omord2lim  44144  cnvtrucl0  44467  eliunov2  44522  iunrelexpmin1  44551  iunrelexpmin2  44555  trclfvcom  44566  cnvtrclfv  44567  trclimalb2  44569  trclfvdecomr  44571  gneispacef2  44979  gneispacern2  44982  gneispace0nelrn  44983  addrval  45291  subrval  45292  mulvval  45293  orbitclmpt  45784  elixpconstg  45924  mptfnd  46074  upbdrech  46141  climf  46455  climf2  46497  liminfval  46590  dvcosre  46743  itgsinexplem1  46785  itgsubsticclem  46806  dmvolss  46816  stoweidlem26  46857  stoweidlem35  46866  stirlinglem14  46918  fourierdlem42  46980  fourierdlem81  47018  fourierdlem89  47026  fourierdlem91  47028  salgenval  47152  elsprel  48378  sprval  48382  prprval  48417  isisubgr  48781  isgrim  48801  uhgrimisgrgric  48850  grtri  48859  isgrlim  48901  usgrexmpl2nb0  48950  usgrexmpl2nb1  48951  usgrexmpl2nb3  48953  upwlksfval  49054  isupwlkg  49056  intopval  49120  clintopval  49122  assintopval  49123  rngcvalALTV  49183  ringcvalALTV  49207  dmatbas  49336  lincop  49341  lcoop  49344  fdivval  49472  blenval  49504  itcoval  49594  itcoval1  49596  itcoval2  49597  itcoval3  49598  itcovalsucov  49601  lines  49664  spheres  49679  discsnterm  50503  termolmd  50599