Theorem elex 3459

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

Syntax hints:   → wi 4   = wceq 1541  ∃wex 1780   ∈ wcel 2113  Vcvv 3438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440

This theorem is referenced by:  elexi  3461  elexd  3462  prcnel  3464  spcimgfi1OLD  3503  vtoclgf  3523  vtocl2gf  3525  vtocl3gf  3526  vtocl2g  3527  vtocl3g  3528  spcgv  3548  spc3egv  3555  elab4g  3636  elrabf  3641  elrab  3644  elrab2w  3648  class2seteq  3660  mob  3673  sbcex  3748  sbcel1v  3804  sbcabel  3826  csbiebt  3876  eldif  3909  elin  3915  ssv  3956  elun  4103  csbnestgfw  4372  sbcco3gw  4375  csbnestgf  4377  sbcco3g  4380  csbco3g  4381  csbvarg  4384  sbccsb2  4387  elpwb  4560  pwidb  4573  elpr2g  4604  snidb  4616  ifpr  4648  snssg  4738  eldifvsn  4751  preqsnd  4813  elpreqpr  4821  dfopg  4825  eluni  4864  eliun  4948  csbexg  5253  nvel  5259  axpweq  5294  reusv2lem4  5344  elopab  5473  epelg  5523  opelvvg  5663  opeliunxp2  5785  opelres  5942  imasng  6041  elimasni  6048  iniseg  6054  inisegn0  6055  dmmptg  6198  elon2  6326  ordsssuc2  6408  iota2  6479  fnmptf  6626  fnmpt  6630  fvelimab  6904  mpteqb  6958  fvmptt  6959  fvmptf  6960  fvopab5  6972  fvopab6  6973  fprg  7098  eloprabga  7465  ovmpos  7504  ov2gf  7505  ovmpox  7509  ovmpoga  7510  ovmpt3rab1  7614  brrpssg  7668  sorpssi  7672  unexgOLD  7692  elpwun  7712  ordeleqon  7725  onintrab  7739  sucexg  7748  sucexeloni  7752  ordsucelsuc  7762  onzsl  7786  dmfexALT  7848  elxp5  7863  fabexg  7878  f1oabexg  7882  offval3  7924  releldm2  7985  fnmpo  8011  mpoexg  8018  bropfvvvv  8032  fsplitfpar  8058  suppval  8102  opeliunxp2f  8150  brtpos2  8172  undefval  8216  tfr2b  8325  tz7.49  8374  oeordi  8513  relelec  8680  ecdmn0  8685  mapvalg  8771  pmvalg  8772  elpmg  8778  elixp2  8837  mptelixpg  8871  elixpsn  8873  2pwuninel  9058  ordfin  9138  rex2dom  9151  fival  9313  elfi2  9315  dffi2  9324  elfiun  9331  wemapso2lem  9455  harval  9463  brwdom  9470  fowdom  9474  brwdom2  9476  brwdom3  9485  en2lp  9513  cantnfsuc  9577  rankvalb  9707  rankwflem  9725  rankr1g  9742  r1pwALT  9756  r1rankid  9769  djulcl  9820  djurcl  9821  inlresf  9824  inrresf  9826  djuss  9830  1stinl  9837  2ndinl  9838  1stinr  9839  2ndinr  9840  cardval3  9862  dfac8alem  9937  isacn  9952  numacn  9957  acndom  9959  cardinfima  10005  unialeph  10009  ackbij1lem5  10131  cflm  10158  isf32lem2  10262  isfin1-2  10293  itunifval  10324  numth3  10378  ttukeylem1  10417  cardidg  10456  ondomon  10471  elwina  10595  elina  10596  wuncval  10651  tskmval  10748  eltskm  10752  recmulnq  10873  elnp  10896  elnpi  10897  npomex  10905  elfzp12  13517  seqp1  13937  hashinf  14256  hashxnn0  14260  hashnn0pnf  14263  hashxrcl  14278  prsshashgt1  14331  hashmap  14356  lsw  14485  ccatfval  14494  ccats1alpha  14541  swrdval  14565  pfxval  14595  splval  14672  splcl  14673  revval  14681  reps  14691  s3sndisj  14888  s3iunsndisj  14889  trclfv  14921  relexp0g  14943  relexpsucnnr  14946  relexp1g  14947  limsupcl  15394  limsupval  15395  clim  15415  rlim  15416  hashbcval  16928  isstruct2  17074  setsvalg  17091  setsfun0  17097  setscom  17105  strfvnd  17110  setsid  17132  ressval  17158  ressinbas  17170  restval  17344  pwsval  17404  xpsfrnel2  17483  ismre  17507  oppcval  17634  oppccatf  17649  brssc  17736  rescval  17749  issubc  17757  isfunc  17786  homadm  17962  homacd  17963  uncfval  18155  pltfval  18250  lubfval  18269  glbfval  18282  joinfval  18292  meetfval  18306  p0val  18346  p1val  18347  oduclatb  18428  ipoval  18451  pws0g  18696  frmdval  18774  vrmdfval  18779  efmnd  18793  efmnd2hash  18817  eqgfval  19103  gaid  19226  cntzfval  19247  elsymgbas  19301  symg2hash  19319  pmtrfval  19377  symggen  19397  gexval  19505  lsmfval  19565  pj1fval  19621  frgpval  19685  vrgpfval  19693  dmdprd  19927  dprdw  19939  pws1  20258  pwsmgp  20260  dvdsr  20296  isrngim  20379  rgspnval  20543  rnghmsscmap  20561  rhmsscmap  20590  lssset  20882  lspfval  20922  islbs  21026  sraval  21125  zlmval  21468  psgnevpmb  21540  ocvfval  21619  cssval  21635  thlval  21648  dsmmval  21687  dsmmbase  21688  frlmval  21701  uvcfval  21737  islinds  21762  ltbval  21996  evlsval  22039  coe1fval  22144  evls1fval  22261  matval  22353  oftpos  22394  dmatval  22434  scmatval  22446  smadiadetglem2  22614  cpmat  22651  mat2pmatfval  22665  cpm2mfval  22691  decpmatval0  22706  pm2mpval  22737  chpmatfval  22772  basdif0  22895  tgval  22897  eltg  22899  eltg2  22900  neipeltop  23071  ordtval  23131  islocfin  23459  txval  23506  qtopval  23637  isfbas  23771  isfildlem  23799  fmval  23885  fmf  23887  isfcls  23951  alexsubb  23988  tsmsfbas  24070  ustval  24145  elutop  24175  isusp  24203  ispsmet  24246  ismet  24265  isxmet  24266  blfvalps  24325  metustel  24492  tngval  24581  elpi1  24999  rrxval  25341  q1peqb  26115  ig1pval  26135  taylfval  26320  ulmval  26343  elno  27611  elnoOLD  27612  nosupno  27669  noetalem2  27708  oldlim  27859  negsval  27994  elzs12  28421  iscgrg  28533  isismt  28555  legval  28605  ishlg  28623  ishpg  28780  iscgra  28830  isinag  28859  isleag  28868  iseqlg  28888  ttgval  28896  xmstrkgc  28907  cplgr2vpr  29455  vtxdgfval  29490  ewlksfval  29624  wksfval  29632  iswlkg  29636  wwlksnon  29873  wspthsnon  29874  avril1  30487  ispligb  30501  gidval  30536  isvcOLD  30603  0vfval  30630  elunop  31896  rabexgfGS  32523  disjdifprg  32599  disjdifprg2  32600  abfmpunirn  32679  rabfmpunirn  32680  hashgt1  32837  indv  32880  mntoval  33013  tocycval  33139  evpmval  33176  altgnsg  33180  sgnsv  33191  inftmrel  33211  isinftm  33212  resvval  33359  ellpi  33403  idlsrgval  33533  rprmval  33546  dimval  33706  dimvalfi  33707  smatfval  33901  lmatval  33919  ispcmp  33963  qqhval2  34088  rrhval  34102  xrhval  34124  esumc  34157  esumpad  34161  esumpcvgval  34184  ofcfval3  34208  issiga  34218  baselsiga  34221  sigasspw  34222  issgon  34229  isrnsigau  34233  sigagenval  34246  ispisys2  34259  cldssbrsiga  34293  sxval  34296  ismeas  34305  cnmbfm  34369  mbfmcnt  34374  elcarsg  34411  sitmval  34455  eulerpartlemt0  34475  sseqval  34494  sseqmw  34497  sseqp1  34501  orvcval  34564  orvcval4  34567  ballotlemsv  34616  prcinf  35218  satf  35496  satfv1lem  35505  satefv  35557  mrexval  35644  mrsubffval  35650  msubffval  35666  mclsval  35706  eldm3  35904  opelco3  35918  elima4  35919  elfix2  36045  elsingles  36059  fvimage  36072  funpartlem  36085  elaltxp  36118  brcolinear2  36201  ellines  36295  topfneec  36498  topfneec2  36499  fnejoin2  36512  limsucncmpi  36588  findabrcl  36597  weiunse  36611  bj-ififc  36725  elelb  37041  bj-pwvrelb  37042  bj-sngltag  37127  bj-xtagex  37133  bj-elsnb  37205  bj-epelg  37212  bj-evalval  37219  bj-ismoore  37249  bj-ideqg1  37308  bj-ideqg1ALT  37309  bj-elid6  37314  bj-diagval  37318  bj-eldiag2  37321  bj-isrvec  37438  finxpreclem1  37533  finxpreclem3  37537  elghomlem2OLD  38026  isrngo  38037  isdivrngo  38090  br1cnvres  38406  riotasv2d  39156  riotasv3d  39159  lshpset  39177  lsatset  39189  lcvfbr  39219  lflset  39258  lkrfval  39286  lkrval2  39289  islshpkrN  39319  ldualset  39324  cmtfvalN  39409  cvrfval  39467  pats  39484  llnset  39704  lplnset  39728  lvolset  39771  lineset  39937  pointsetN  39940  psubspset  39943  pmapfval  39955  paddfval  39996  pclfvalN  40088  polfvalN  40103  psubclsetN  40135  watfvalN  40191  lhpset  40194  lautset  40281  pautsetN  40297  ldilfset  40307  ltrnfset  40316  dilfsetN  40351  trnfsetN  40354  trlfset  40359  tgrpfset  40943  tendofset  40957  erngfset  40998  erngfset-rN  41006  dvafset  41203  diaffval  41229  dvhfset  41279  docaffvalN  41320  djaffvalN  41332  dibffval  41339  dicffval  41373  dihffval  41429  dochffval  41548  djhffval  41595  lpolsetN  41681  lcdfval  41787  mapdffval  41825  hvmapffval  41957  hdmap1ffval  41994  hdmapffval  42025  hgmapffval  42084  hlhilset  42133  elrfi  42878  nacsfix  42896  mapfzcons2  42903  sbc2rexgOLD  42972  sbc4rexgOLD  42974  setindtrs  43209  wepwso  43227  hbtlem1  43307  hbtlem7  43309  mendval  43363  oaltublim  43474  omord2lim  43484  cnvtrucl0  43807  eliunov2  43862  iunrelexpmin1  43891  iunrelexpmin2  43895  trclfvcom  43906  cnvtrclfv  43907  trclimalb2  43909  trclfvdecomr  43911  gneispacef2  44319  gneispacern2  44322  gneispace0nelrn  44323  addrval  44648  subrval  44649  mulvval  44650  orbitclmpt  45141  elixpconstg  45275  mptfnd  45428  upbdrech  45495  climf  45810  climf2  45852  liminfval  45945  dvcosre  46098  itgsinexplem1  46140  itgsubsticclem  46161  dmvolss  46171  stoweidlem26  46212  stoweidlem35  46221  stirlinglem14  46273  fourierdlem42  46335  fourierdlem81  46373  fourierdlem89  46381  fourierdlem91  46383  salgenval  46507  elsprel  47663  sprval  47667  prprval  47702  isisubgr  48050  isgrim  48070  uhgrimisgrgric  48119  grtri  48128  isgrlim  48170  usgrexmpl2nb0  48219  usgrexmpl2nb1  48220  usgrexmpl2nb3  48222  upwlksfval  48323  isupwlkg  48325  intopval  48390  clintopval  48392  assintopval  48393  rngcvalALTV  48453  ringcvalALTV  48477  dmatbas  48591  lincop  48596  lcoop  48599  fdivval  48727  blenval  48759  itcoval  48849  itcoval1  48851  itcoval2  48852  itcoval3  48853  itcovalsucov  48856  lines  48919  spheres  48934  discsnterm  49761  termolmd  49857