Theorem elex 3452

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

Syntax hints:   → wi 4   = wceq 1547  ∃wex 1786   ∈ wcel 2119  Vcvv 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433

This theorem is referenced by:  elexi  3453  elexd  3454  prcnel  3456  spcimgfi1OLD  3494  vtoclgf  3513  vtocl2gf  3515  vtocl3gf  3516  vtocl2g  3517  vtocl3g  3518  spcgv  3534  spc3egv  3541  elab4g  3621  elrabf  3626  elrab  3629  elrab2w  3633  class2seteq  3645  mob  3658  sbcex  3733  sbcel1v  3788  sbcabel  3810  csbiebt  3860  eldif  3893  elin  3899  ssv  3939  elun  4083  csbnestgfw  4350  sbcco3gw  4353  csbnestgf  4355  sbcco3g  4358  csbco3g  4359  csbvarg  4362  sbccsb2  4365  elpwb  4537  pwidb  4550  elpr2g  4581  snidb  4593  ifpr  4625  snssg  4715  eldifvsn  4730  preqsnd  4790  elpreqpr  4798  dfopg  4802  eluni  4841  eliun  4925  csbexg  5232  nvelOLD  5244  axpweq  5279  reusv2lem4  5330  elopab  5469  epelg  5519  opelvvg  5659  opeliunxp2  5780  opelres  5937  imasng  6036  elimasni  6043  iniseg  6049  inisegn0  6050  dmmptg  6193  elon2  6321  ordsssuc2  6403  iota2  6474  fnmptf  6621  fnmpt  6625  fvelimab  6899  mpteqb  6955  fvmptt  6956  fvmptf  6957  fvopab5  6969  fvopab6  6970  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  8031  fsplitfpar  8057  suppval  8102  opeliunxp2f  8150  brtpos2  8172  undefval  8216  tfr2b  8325  tz7.49  8374  oeordi  8513  relelec  8681  ecdmn0  8686  mapvalg  8773  pmvalg  8774  elpmg  8780  elixp2  8839  mptelixpg  8873  elixpsn  8875  2pwuninel  9060  ordfin  9140  rex2dom  9153  fival  9315  elfi2  9317  dffi2  9326  elfiun  9333  wemapso2lem  9457  harval  9465  brwdom  9472  fowdom  9476  brwdom2  9478  brwdom3  9487  en2lp  9518  cantnfsuc  9582  rankvalb  9712  rankwflem  9730  rankr1g  9747  r1pwALT  9761  r1rankid  9774  djulcl  9825  djurcl  9826  inlresf  9829  inrresf  9831  djuss  9835  1stinl  9842  2ndinl  9843  1stinr  9844  2ndinr  9845  cardval3  9867  dfac8alem  9942  isacn  9957  numacn  9962  acndom  9964  cardinfima  10010  unialeph  10014  ackbij1lem5  10136  cflm  10163  isf32lem2  10267  isfin1-2  10298  itunifval  10329  numth3  10383  ttukeylem1  10422  cardidg  10461  ondomon  10476  elwina  10600  elina  10601  wuncval  10656  tskmval  10753  eltskm  10757  recmulnq  10878  elnp  10901  elnpi  10902  npomex  10910  indv  12152  elfzp12  13548  seqp1  13969  hashinf  14288  hashxnn0  14292  hashnn0pnf  14295  hashxrcl  14310  prsshashgt1  14363  hashmap  14388  lsw  14517  ccatfval  14526  ccats1alpha  14573  swrdval  14597  pfxval  14627  splval  14704  splcl  14705  revval  14713  reps  14723  s3sndisj  14920  s3iunsndisj  14921  trclfv  14953  relexp0g  14975  relexpsucnnr  14978  relexp1g  14979  limsupcl  15426  limsupval  15427  clim  15447  rlim  15448  hashbcval  16964  isstruct2  17110  setsvalg  17127  setsfun0  17133  setscom  17141  strfvnd  17146  setsid  17168  ressval  17194  ressinbas  17206  restval  17380  pwsval  17440  xpsfrnel2  17519  ismre  17543  oppcval  17670  oppccatf  17685  brssc  17772  rescval  17785  issubc  17793  isfunc  17822  homadm  17998  homacd  17999  uncfval  18191  pltfval  18286  lubfval  18305  glbfval  18318  joinfval  18328  meetfval  18342  p0val  18382  p1val  18383  oduclatb  18464  ipoval  18487  pws0g  18732  frmdval  18810  vrmdfval  18815  efmnd  18829  efmnd2hash  18853  eqgfval  19142  gaid  19265  cntzfval  19286  elsymgbas  19340  symg2hash  19358  pmtrfval  19416  symggen  19436  gexval  19544  lsmfval  19604  pj1fval  19660  frgpval  19724  vrgpfval  19732  dmdprd  19966  dprdw  19978  pws1  20295  pwsmgp  20297  dvdsr  20333  isrngim  20416  rgspnval  20584  rnghmsscmap  20602  rhmsscmap  20631  lssset  20923  lspfval  20963  islbs  21066  sraval  21165  zlmval  21490  psgnevpmb  21562  ocvfval  21641  cssval  21657  thlval  21670  dsmmval  21709  dsmmbase  21710  frlmval  21723  uvcfval  21759  islinds  21784  ltbval  22019  evlsval  22062  coe1fval  22190  evls1fval  22305  matval  22394  oftpos  22435  dmatval  22475  scmatval  22487  smadiadetglem2  22655  cpmat  22692  mat2pmatfval  22706  cpm2mfval  22732  decpmatval0  22747  pm2mpval  22778  chpmatfval  22813  basdif0  22936  tgval  22938  eltg  22940  eltg2  22941  neipeltop  23112  ordtval  23172  islocfin  23500  txval  23547  qtopval  23678  isfbas  23812  isfildlem  23840  fmval  23926  fmf  23928  isfcls  23992  alexsubb  24029  tsmsfbas  24111  ustval  24186  elutop  24216  isusp  24244  ispsmet  24287  ismet  24306  isxmet  24307  blfvalps  24366  metustel  24533  tngval  24622  elpi1  25030  rrxval  25372  q1peqb  26139  ig1pval  26159  taylfval  26342  ulmval  26363  elno  27627  elnoOLD  27628  nosupno  27685  noetalem2  27724  nulslts  27785  oldlim  27897  negsval  28035  elz12s  28482  iscgrg  28598  isismt  28620  legval  28670  ishlg  28688  ishpg  28845  iscgra  28895  isinag  28924  isleag  28933  iseqlg  28953  ttgval  28961  xmstrkgc  28972  cplgr2vpr  29520  vtxdgfval  29554  ewlksfval  29688  wksfval  29696  iswlkg  29700  wwlksnon  29937  wspthsnon  29938  avril1  30551  ispligb  30566  gidval  30601  isvcOLD  30668  0vfval  30695  elunop  31961  rabexgfGS  32587  disjdifprg  32664  disjdifprg2  32665  abfmpunirn  32744  rabfmpunirn  32745  hashgt1  32900  mntoval  33061  tocycval  33189  evpmval  33226  altgnsg  33230  sgnsv  33241  inftmrel  33261  isinftm  33262  resvval  33412  ellpi  33456  idlsrgval  33586  rprmval  33599  dimval  33785  dimvalfi  33786  smatfval  33979  lmatval  33997  ispcmp  34041  qqhval2  34166  rrhval  34180  xrhval  34202  esumc  34235  esumpad  34239  esumpcvgval  34262  ofcfval3  34286  issiga  34296  baselsiga  34299  sigasspw  34300  issgon  34307  isrnsigau  34311  sigagenval  34324  ispisys2  34337  cldssbrsiga  34371  sxval  34374  ismeas  34383  cnmbfm  34447  mbfmcnt  34452  elcarsg  34489  sitmval  34533  eulerpartlemt0  34553  sseqval  34572  sseqmw  34575  sseqp1  34579  orvcval  34642  orvcval4  34645  ballotlemsv  34694  prcinf  35294  satf  35581  satfv1lem  35590  satefv  35642  mrexval  35729  mrsubffval  35735  msubffval  35751  mclsval  35791  eldm3  35989  opelco3  36003  elima4  36004  elfix2  36130  elsingles  36144  fvimage  36157  funpartlem  36170  elaltxp  36203  brcolinear2  36286  ellines  36380  topfneec  36583  topfneec2  36584  fnejoin2  36597  limsucncmpi  36673  findabrcl  36682  weiunse  36696  ttcwf2  36753  bj-ififc  36893  elelb  37250  bj-pwvrelb  37251  bj-sngltag  37336  bj-xtagex  37342  bj-elsnb  37414  bj-epelg  37421  bj-evalval  37433  bj-ismoore  37463  bj-ideqg1  37524  bj-ideqg1ALT  37525  bj-elid6  37530  bj-diagval  37534  bj-eldiag2  37537  bj-isrvec  37654  finxpreclem1  37751  finxpreclem3  37755  elghomlem2OLD  38253  isrngo  38264  isdivrngo  38317  br1cnvres  38641  riotasv2d  39449  riotasv3d  39452  lshpset  39470  lsatset  39482  lcvfbr  39512  lflset  39551  lkrfval  39579  lkrval2  39582  islshpkrN  39612  ldualset  39617  cmtfvalN  39702  cvrfval  39760  pats  39777  llnset  39997  lplnset  40021  lvolset  40064  lineset  40230  pointsetN  40233  psubspset  40236  pmapfval  40248  paddfval  40289  pclfvalN  40381  polfvalN  40396  psubclsetN  40428  watfvalN  40484  lhpset  40487  lautset  40574  pautsetN  40590  ldilfset  40600  ltrnfset  40609  dilfsetN  40644  trnfsetN  40647  trlfset  40652  tgrpfset  41236  tendofset  41250  erngfset  41291  erngfset-rN  41299  dvafset  41496  diaffval  41522  dvhfset  41572  docaffvalN  41613  djaffvalN  41625  dibffval  41632  dicffval  41666  dihffval  41722  dochffval  41841  djhffval  41888  lpolsetN  41974  lcdfval  42080  mapdffval  42118  hvmapffval  42250  hdmap1ffval  42287  hdmapffval  42318  hgmapffval  42377  hlhilset  42426  elrfi  43143  nacsfix  43161  mapfzcons2  43168  setindtrs  43470  wepwso  43488  hbtlem1  43568  hbtlem7  43570  mendval  43624  oaltublim  43735  omord2lim  43745  cnvtrucl0  44068  eliunov2  44123  iunrelexpmin1  44152  iunrelexpmin2  44156  trclfvcom  44167  cnvtrclfv  44168  trclimalb2  44170  trclfvdecomr  44172  gneispacef2  44580  gneispacern2  44583  gneispace0nelrn  44584  addrval  44909  subrval  44910  mulvval  44911  orbitclmpt  45402  elixpconstg  45536  mptfnd  45686  upbdrech  45753  climf  46067  climf2  46109  liminfval  46202  dvcosre  46355  itgsinexplem1  46397  itgsubsticclem  46418  dmvolss  46428  stoweidlem26  46469  stoweidlem35  46478  stirlinglem14  46530  fourierdlem42  46592  fourierdlem81  46630  fourierdlem89  46638  fourierdlem91  46640  salgenval  46764  elsprel  47950  sprval  47954  prprval  47989  isisubgr  48353  isgrim  48373  uhgrimisgrgric  48422  grtri  48431  isgrlim  48473  usgrexmpl2nb0  48522  usgrexmpl2nb1  48523  usgrexmpl2nb3  48525  upwlksfval  48626  isupwlkg  48628  intopval  48693  clintopval  48695  assintopval  48696  rngcvalALTV  48756  ringcvalALTV  48780  dmatbas  48894  lincop  48899  lcoop  48902  fdivval  49030  blenval  49062  itcoval  49152  itcoval1  49154  itcoval2  49155  itcoval3  49156  itcovalsucov  49159  lines  49222  spheres  49237  discsnterm  50064  termolmd  50160