Theorem elex 3451

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

Syntax hints:   → wi 4   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432

This theorem is referenced by:  elexi  3453  elexd  3454  prcnel  3456  spcimgfi1OLD  3494  vtoclgf  3514  vtocl2gf  3516  vtocl3gf  3517  vtocl2g  3518  vtocl3g  3519  spcgv  3539  spc3egv  3546  elab4g  3627  elrabf  3632  elrab  3635  elrab2w  3639  class2seteq  3651  mob  3664  sbcex  3739  sbcel1v  3795  sbcabel  3817  csbiebt  3867  eldif  3900  elin  3906  ssv  3947  elun  4094  csbnestgfw  4363  sbcco3gw  4366  csbnestgf  4368  sbcco3g  4371  csbco3g  4372  csbvarg  4375  sbccsb2  4378  elpwb  4550  pwidb  4563  elpr2g  4594  snidb  4606  ifpr  4638  snssg  4728  eldifvsn  4741  preqsnd  4803  elpreqpr  4811  dfopg  4815  eluni  4854  eliun  4938  csbexg  5246  nvel  5254  axpweq  5289  reusv2lem4  5339  elopab  5476  epelg  5526  opelvvg  5666  opeliunxp2  5788  opelres  5945  imasng  6044  elimasni  6051  iniseg  6057  inisegn0  6058  dmmptg  6201  elon2  6329  ordsssuc2  6411  iota2  6482  fnmptf  6629  fnmpt  6633  fvelimab  6907  mpteqb  6962  fvmptt  6963  fvmptf  6964  fvopab5  6976  fvopab6  6977  fprg  7103  eloprabga  7470  ovmpos  7509  ov2gf  7510  ovmpox  7514  ovmpoga  7515  ovmpt3rab1  7619  brrpssg  7673  sorpssi  7677  unexgOLD  7697  elpwun  7717  ordeleqon  7730  onintrab  7744  sucexg  7753  sucexeloni  7757  ordsucelsuc  7767  onzsl  7791  dmfexALT  7853  elxp5  7868  fabexg  7883  f1oabexg  7887  offval3  7929  releldm2  7990  fnmpo  8016  mpoexg  8023  bropfvvvv  8036  fsplitfpar  8062  suppval  8106  opeliunxp2f  8154  brtpos2  8176  undefval  8220  tfr2b  8329  tz7.49  8378  oeordi  8517  relelec  8685  ecdmn0  8690  mapvalg  8777  pmvalg  8778  elpmg  8784  elixp2  8843  mptelixpg  8877  elixpsn  8879  2pwuninel  9064  ordfin  9144  rex2dom  9157  fival  9319  elfi2  9321  dffi2  9330  elfiun  9337  wemapso2lem  9461  harval  9469  brwdom  9476  fowdom  9480  brwdom2  9482  brwdom3  9491  en2lp  9521  cantnfsuc  9585  rankvalb  9715  rankwflem  9733  rankr1g  9750  r1pwALT  9764  r1rankid  9777  djulcl  9828  djurcl  9829  inlresf  9832  inrresf  9834  djuss  9838  1stinl  9845  2ndinl  9846  1stinr  9847  2ndinr  9848  cardval3  9870  dfac8alem  9945  isacn  9960  numacn  9965  acndom  9967  cardinfima  10013  unialeph  10017  ackbij1lem5  10139  cflm  10166  isf32lem2  10270  isfin1-2  10301  itunifval  10332  numth3  10386  ttukeylem1  10425  cardidg  10464  ondomon  10479  elwina  10603  elina  10604  wuncval  10659  tskmval  10756  eltskm  10760  recmulnq  10881  elnp  10904  elnpi  10905  npomex  10913  indv  12155  elfzp12  13551  seqp1  13972  hashinf  14291  hashxnn0  14295  hashnn0pnf  14298  hashxrcl  14313  prsshashgt1  14366  hashmap  14391  lsw  14520  ccatfval  14529  ccats1alpha  14576  swrdval  14600  pfxval  14630  splval  14707  splcl  14708  revval  14716  reps  14726  s3sndisj  14923  s3iunsndisj  14924  trclfv  14956  relexp0g  14978  relexpsucnnr  14981  relexp1g  14982  limsupcl  15429  limsupval  15430  clim  15450  rlim  15451  hashbcval  16967  isstruct2  17113  setsvalg  17130  setsfun0  17136  setscom  17144  strfvnd  17149  setsid  17171  ressval  17197  ressinbas  17209  restval  17383  pwsval  17443  xpsfrnel2  17522  ismre  17546  oppcval  17673  oppccatf  17688  brssc  17775  rescval  17788  issubc  17796  isfunc  17825  homadm  18001  homacd  18002  uncfval  18194  pltfval  18289  lubfval  18308  glbfval  18321  joinfval  18331  meetfval  18345  p0val  18385  p1val  18386  oduclatb  18467  ipoval  18490  pws0g  18735  frmdval  18813  vrmdfval  18818  efmnd  18832  efmnd2hash  18856  eqgfval  19145  gaid  19268  cntzfval  19289  elsymgbas  19343  symg2hash  19361  pmtrfval  19419  symggen  19439  gexval  19547  lsmfval  19607  pj1fval  19663  frgpval  19727  vrgpfval  19735  dmdprd  19969  dprdw  19981  pws1  20298  pwsmgp  20300  dvdsr  20336  isrngim  20419  rgspnval  20583  rnghmsscmap  20601  rhmsscmap  20630  lssset  20922  lspfval  20962  islbs  21066  sraval  21165  zlmval  21508  psgnevpmb  21580  ocvfval  21659  cssval  21675  thlval  21688  dsmmval  21727  dsmmbase  21728  frlmval  21741  uvcfval  21777  islinds  21802  ltbval  22034  evlsval  22077  coe1fval  22182  evls1fval  22297  matval  22389  oftpos  22430  dmatval  22470  scmatval  22482  smadiadetglem2  22650  cpmat  22687  mat2pmatfval  22701  cpm2mfval  22727  decpmatval0  22742  pm2mpval  22773  chpmatfval  22808  basdif0  22931  tgval  22933  eltg  22935  eltg2  22936  neipeltop  23107  ordtval  23167  islocfin  23495  txval  23542  qtopval  23673  isfbas  23807  isfildlem  23835  fmval  23921  fmf  23923  isfcls  23987  alexsubb  24024  tsmsfbas  24106  ustval  24181  elutop  24211  isusp  24239  ispsmet  24282  ismet  24301  isxmet  24302  blfvalps  24361  metustel  24528  tngval  24617  elpi1  25025  rrxval  25367  q1peqb  26134  ig1pval  26154  taylfval  26338  ulmval  26361  elno  27626  elnoOLD  27627  nosupno  27684  noetalem2  27723  nulslts  27784  oldlim  27896  negsval  28034  elz12s  28481  iscgrg  28597  isismt  28619  legval  28669  ishlg  28687  ishpg  28844  iscgra  28894  isinag  28923  isleag  28932  iseqlg  28952  ttgval  28960  xmstrkgc  28971  cplgr2vpr  29519  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  32663  disjdifprg2  32664  abfmpunirn  32743  rabfmpunirn  32744  hashgt1  32899  mntoval  33060  tocycval  33187  evpmval  33224  altgnsg  33228  sgnsv  33239  inftmrel  33259  isinftm  33260  resvval  33407  ellpi  33451  idlsrgval  33581  rprmval  33594  dimval  33763  dimvalfi  33764  smatfval  33958  lmatval  33976  ispcmp  34020  qqhval2  34145  rrhval  34159  xrhval  34181  esumc  34214  esumpad  34218  esumpcvgval  34241  ofcfval3  34265  issiga  34275  baselsiga  34278  sigasspw  34279  issgon  34286  isrnsigau  34290  sigagenval  34303  ispisys2  34316  cldssbrsiga  34350  sxval  34353  ismeas  34362  cnmbfm  34426  mbfmcnt  34431  elcarsg  34468  sitmval  34512  eulerpartlemt0  34532  sseqval  34551  sseqmw  34554  sseqp1  34558  orvcval  34621  orvcval4  34624  ballotlemsv  34673  prcinf  35276  satf  35554  satfv1lem  35563  satefv  35615  mrexval  35702  mrsubffval  35708  msubffval  35724  mclsval  35764  eldm3  35962  opelco3  35976  elima4  35977  elfix2  36103  elsingles  36117  fvimage  36130  funpartlem  36143  elaltxp  36176  brcolinear2  36259  ellines  36353  topfneec  36556  topfneec2  36557  fnejoin2  36570  limsucncmpi  36646  findabrcl  36655  weiunse  36669  ttcwf2  36726  bj-ififc  36866  elelb  37223  bj-pwvrelb  37224  bj-sngltag  37309  bj-xtagex  37315  bj-elsnb  37387  bj-epelg  37394  bj-evalval  37406  bj-ismoore  37436  bj-ideqg1  37497  bj-ideqg1ALT  37498  bj-elid6  37503  bj-diagval  37507  bj-eldiag2  37510  bj-isrvec  37627  finxpreclem1  37722  finxpreclem3  37726  elghomlem2OLD  38224  isrngo  38235  isdivrngo  38288  br1cnvres  38612  riotasv2d  39420  riotasv3d  39423  lshpset  39441  lsatset  39453  lcvfbr  39483  lflset  39522  lkrfval  39550  lkrval2  39553  islshpkrN  39583  ldualset  39588  cmtfvalN  39673  cvrfval  39731  pats  39748  llnset  39968  lplnset  39992  lvolset  40035  lineset  40201  pointsetN  40204  psubspset  40207  pmapfval  40219  paddfval  40260  pclfvalN  40352  polfvalN  40367  psubclsetN  40399  watfvalN  40455  lhpset  40458  lautset  40545  pautsetN  40561  ldilfset  40571  ltrnfset  40580  dilfsetN  40615  trnfsetN  40618  trlfset  40623  tgrpfset  41207  tendofset  41221  erngfset  41262  erngfset-rN  41270  dvafset  41467  diaffval  41493  dvhfset  41543  docaffvalN  41584  djaffvalN  41596  dibffval  41603  dicffval  41637  dihffval  41693  dochffval  41812  djhffval  41859  lpolsetN  41945  lcdfval  42051  mapdffval  42089  hvmapffval  42221  hdmap1ffval  42258  hdmapffval  42289  hgmapffval  42348  hlhilset  42397  elrfi  43143  nacsfix  43161  mapfzcons2  43168  sbc2rexgOLD  43237  sbc4rexgOLD  43239  setindtrs  43474  wepwso  43492  hbtlem1  43572  hbtlem7  43574  mendval  43628  oaltublim  43739  omord2lim  43749  cnvtrucl0  44072  eliunov2  44127  iunrelexpmin1  44156  iunrelexpmin2  44160  trclfvcom  44171  cnvtrclfv  44172  trclimalb2  44174  trclfvdecomr  44176  gneispacef2  44584  gneispacern2  44587  gneispace0nelrn  44588  addrval  44913  subrval  44914  mulvval  44915  orbitclmpt  45406  elixpconstg  45540  mptfnd  45692  upbdrech  45759  climf  46073  climf2  46115  liminfval  46208  dvcosre  46361  itgsinexplem1  46403  itgsubsticclem  46424  dmvolss  46434  stoweidlem26  46475  stoweidlem35  46484  stirlinglem14  46536  fourierdlem42  46598  fourierdlem81  46636  fourierdlem89  46644  fourierdlem91  46646  salgenval  46770  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