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

Syntax hints:   → wi 4   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Vcvv 3450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452

This theorem is referenced by:  elexi  3473  elexd  3474  prcnel  3476  spcimgfi1OLD  3517  vtoclgf  3538  vtocl2gf  3541  vtocl3gf  3542  vtocl2g  3543  vtocl3g  3544  spcgv  3565  spc3egv  3572  elab4g  3653  elrabf  3658  elrab  3662  elrab2w  3666  class2seteq  3678  mob  3691  sbcex  3766  sbcel1v  3822  sbcabel  3844  csbiebt  3894  eldif  3927  elin  3933  ssv  3974  elun  4119  csbnestgfw  4388  sbcco3gw  4391  csbnestgf  4393  sbcco3g  4396  csbco3g  4397  csbvarg  4400  sbccsb2  4403  elpwb  4574  pwidb  4587  elpr2g  4618  snidb  4628  ifpr  4660  snssg  4750  eldifvsn  4764  preqsnd  4826  elpreqpr  4834  dfopg  4838  eluni  4877  eliun  4962  csbexg  5268  nvel  5274  axpweq  5309  reusv2lem4  5359  elopab  5490  epelg  5542  opelvvg  5682  opeliunxp2  5805  opelres  5959  imasng  6058  elimasni  6065  iniseg  6071  inisegn0  6072  dmmptg  6218  elon2  6346  ordsssuc2  6428  iota2  6503  fnmptf  6657  fnmpt  6661  fvelimab  6936  mpteqb  6990  fvmptt  6991  fvmptf  6992  fvopab5  7004  fvopab6  7005  fprg  7130  eloprabga  7501  ovmpos  7540  ov2gf  7541  ovmpox  7545  ovmpoga  7546  ovmpt3rab1  7650  brrpssg  7704  sorpssi  7708  unexgOLD  7728  elpwun  7748  ordeleqon  7761  onintrab  7775  sucexg  7784  sucexeloni  7788  ordsucelsuc  7800  onzsl  7825  dmfexALT  7887  elxp5  7902  fabexg  7917  f1oabexg  7921  offval3  7964  releldm2  8025  fnmpo  8051  mpoexg  8058  mptmpoopabbrdOLDOLD  8065  bropfvvvv  8074  fsplitfpar  8100  suppval  8144  opeliunxp2f  8192  brtpos2  8214  undefval  8258  tfr2b  8367  tz7.49  8416  oeordi  8554  relelec  8721  ecdmn0  8726  mapvalg  8812  pmvalg  8813  elpmg  8819  elixp2  8877  mptelixpg  8911  elixpsn  8913  2pwuninel  9102  rex2dom  9200  fival  9370  elfi2  9372  dffi2  9381  elfiun  9388  wemapso2lem  9512  harval  9520  brwdom  9527  fowdom  9531  brwdom2  9533  brwdom3  9542  en2lp  9566  cantnfsuc  9630  rankvalb  9757  rankwflem  9775  rankr1g  9792  r1pwALT  9806  r1rankid  9819  djulcl  9870  djurcl  9871  inlresf  9874  inrresf  9876  djuss  9880  1stinl  9887  2ndinl  9888  1stinr  9889  2ndinr  9890  cardval3  9912  dfac8alem  9989  isacn  10004  numacn  10009  acndom  10011  cardinfima  10057  unialeph  10061  ackbij1lem5  10183  cflm  10210  isf32lem2  10314  isfin1-2  10345  itunifval  10376  numth3  10430  ttukeylem1  10469  cardidg  10508  ondomon  10523  elwina  10646  elina  10647  wuncval  10702  tskmval  10799  eltskm  10803  recmulnq  10924  elnp  10947  elnpi  10948  npomex  10956  elfzp12  13571  seqp1  13988  hashinf  14307  hashxnn0  14311  hashnn0pnf  14314  hashxrcl  14329  prsshashgt1  14382  hashmap  14407  lsw  14536  ccatfval  14545  ccats1alpha  14591  swrdval  14615  pfxval  14645  splval  14723  splcl  14724  revval  14732  reps  14742  s3sndisj  14940  s3iunsndisj  14941  trclfv  14973  relexp0g  14995  relexpsucnnr  14998  relexp1g  14999  limsupcl  15446  limsupval  15447  clim  15467  rlim  15468  hashbcval  16980  isstruct2  17126  setsvalg  17143  setsfun0  17149  setscom  17157  strfvnd  17162  setsid  17184  ressval  17210  ressinbas  17222  restval  17396  pwsval  17456  xpsfrnel2  17534  ismre  17558  oppcval  17681  oppccatf  17696  brssc  17783  rescval  17796  issubc  17804  isfunc  17833  homadm  18009  homacd  18010  uncfval  18202  pltfval  18297  lubfval  18316  glbfval  18329  joinfval  18339  meetfval  18353  p0val  18393  p1val  18394  oduclatb  18473  ipoval  18496  pws0g  18707  frmdval  18785  vrmdfval  18790  efmnd  18804  efmnd2hash  18828  eqgfval  19115  gaid  19238  cntzfval  19259  elsymgbas  19311  symg2hash  19329  pmtrfval  19387  symggen  19407  gexval  19515  lsmfval  19575  pj1fval  19631  frgpval  19695  vrgpfval  19703  dmdprd  19937  dprdw  19949  pws1  20241  pwsmgp  20243  dvdsr  20278  isrngim  20361  isrim0OLD  20397  rgspnval  20528  rnghmsscmap  20546  rhmsscmap  20575  lssset  20846  lspfval  20886  islbs  20990  sraval  21089  zlmval  21432  psgnevpmb  21503  ocvfval  21582  cssval  21598  thlval  21611  dsmmval  21650  dsmmbase  21651  frlmval  21664  uvcfval  21700  islinds  21725  ltbval  21957  evlsval  22000  coe1fval  22097  evls1fval  22213  matval  22305  oftpos  22346  dmatval  22386  scmatval  22398  smadiadetglem2  22566  cpmat  22603  mat2pmatfval  22617  cpm2mfval  22643  decpmatval0  22658  pm2mpval  22689  chpmatfval  22724  basdif0  22847  tgval  22849  eltg  22851  eltg2  22852  neipeltop  23023  ordtval  23083  islocfin  23411  txval  23458  qtopval  23589  isfbas  23723  isfildlem  23751  fmval  23837  fmf  23839  isfcls  23903  alexsubb  23940  tsmsfbas  24022  ustval  24097  elutop  24128  isusp  24156  ispsmet  24199  ismet  24218  isxmet  24219  blfvalps  24278  metustel  24445  tngval  24534  elpi1  24952  rrxval  25294  q1peqb  26068  ig1pval  26088  taylfval  26273  ulmval  26296  elno  27564  elnoOLD  27565  nosupno  27622  noetalem2  27661  oldlim  27805  negsval  27938  elzs12  28344  iscgrg  28446  isismt  28468  legval  28518  ishlg  28536  ishpg  28693  iscgra  28743  isinag  28772  isleag  28781  iseqlg  28801  ttgval  28809  xmstrkgc  28820  cplgr2vpr  29367  vtxdgfval  29402  ewlksfval  29536  wksfval  29544  iswlkg  29548  wwlksnon  29788  wspthsnon  29789  avril1  30399  ispligb  30413  gidval  30448  isvcOLD  30515  0vfval  30542  elunop  31808  rabexgfGS  32435  disjdifprg  32511  disjdifprg2  32512  abfmpunirn  32583  rabfmpunirn  32584  hashgt1  32740  indv  32782  mntoval  32915  tocycval  33072  evpmval  33109  altgnsg  33113  sgnsv  33124  inftmrel  33141  isinftm  33142  resvval  33308  ellpi  33351  idlsrgval  33481  rprmval  33494  dimval  33603  dimvalfi  33604  smatfval  33792  lmatval  33810  ispcmp  33854  qqhval2  33979  rrhval  33993  xrhval  34015  esumc  34048  esumpad  34052  esumpcvgval  34075  ofcfval3  34099  issiga  34109  baselsiga  34112  sigasspw  34113  issgon  34120  isrnsigau  34124  sigagenval  34137  ispisys2  34150  cldssbrsiga  34184  sxval  34187  ismeas  34196  cnmbfm  34261  mbfmcnt  34266  elcarsg  34303  sitmval  34347  eulerpartlemt0  34367  sseqval  34386  sseqmw  34389  sseqp1  34393  orvcval  34456  orvcval4  34459  ballotlemsv  34508  prcinf  35091  satf  35347  satfv1lem  35356  satefv  35408  mrexval  35495  mrsubffval  35501  msubffval  35517  mclsval  35557  eldm3  35755  opelco3  35769  elima4  35770  elfix2  35899  elsingles  35913  fvimage  35926  funpartlem  35937  elaltxp  35970  brcolinear2  36053  ellines  36147  topfneec  36350  topfneec2  36351  fnejoin2  36364  limsucncmpi  36440  findabrcl  36449  weiunse  36463  bj-ififc  36577  elelb  36892  bj-pwvrelb  36893  bj-sngltag  36978  bj-xtagex  36984  bj-elsnb  37056  bj-epelg  37063  bj-evalval  37070  bj-ismoore  37100  bj-ideqg1  37159  bj-ideqg1ALT  37160  bj-elid6  37165  bj-diagval  37169  bj-eldiag2  37172  bj-isrvec  37289  finxpreclem1  37384  finxpreclem3  37388  elghomlem2OLD  37887  isrngo  37898  isdivrngo  37951  br1cnvres  38265  riotasv2d  38957  riotasv3d  38960  lshpset  38978  lsatset  38990  lcvfbr  39020  lflset  39059  lkrfval  39087  lkrval2  39090  islshpkrN  39120  ldualset  39125  cmtfvalN  39210  cvrfval  39268  pats  39285  llnset  39506  lplnset  39530  lvolset  39573  lineset  39739  pointsetN  39742  psubspset  39745  pmapfval  39757  paddfval  39798  pclfvalN  39890  polfvalN  39905  psubclsetN  39937  watfvalN  39993  lhpset  39996  lautset  40083  pautsetN  40099  ldilfset  40109  ltrnfset  40118  dilfsetN  40153  trnfsetN  40156  trlfset  40161  tgrpfset  40745  tendofset  40759  erngfset  40800  erngfset-rN  40808  dvafset  41005  diaffval  41031  dvhfset  41081  docaffvalN  41122  djaffvalN  41134  dibffval  41141  dicffval  41175  dihffval  41231  dochffval  41350  djhffval  41397  lpolsetN  41483  lcdfval  41589  mapdffval  41627  hvmapffval  41759  hdmap1ffval  41796  hdmapffval  41827  hgmapffval  41886  hlhilset  41935  elrfi  42689  nacsfix  42707  mapfzcons2  42714  sbc2rexgOLD  42783  sbc4rexgOLD  42785  setindtrs  43021  wepwso  43039  hbtlem1  43119  hbtlem7  43121  mendval  43175  oaltublim  43286  omord2lim  43296  cnvtrucl0  43620  eliunov2  43675  iunrelexpmin1  43704  iunrelexpmin2  43708  trclfvcom  43719  cnvtrclfv  43720  trclimalb2  43722  trclfvdecomr  43724  gneispacef2  44132  gneispacern2  44135  gneispace0nelrn  44136  addrval  44462  subrval  44463  mulvval  44464  orbitclmpt  44955  elixpconstg  45090  mptfnd  45243  upbdrech  45310  climf  45627  climf2  45671  liminfval  45764  dvcosre  45917  itgsinexplem1  45959  itgsubsticclem  45980  dmvolss  45990  stoweidlem26  46031  stoweidlem35  46040  stirlinglem14  46092  fourierdlem42  46154  fourierdlem81  46192  fourierdlem89  46200  fourierdlem91  46202  salgenval  46326  elsprel  47480  sprval  47484  prprval  47519  isisubgr  47866  isgrim  47886  uhgrimisgrgric  47935  grtri  47943  isgrlim  47985  usgrexmpl2nb0  48026  usgrexmpl2nb1  48027  usgrexmpl2nb3  48029  upwlksfval  48127  isupwlkg  48129  intopval  48194  clintopval  48196  assintopval  48197  rngcvalALTV  48257  ringcvalALTV  48281  dmatbas  48396  lincop  48401  lcoop  48404  fdivval  48532  blenval  48564  itcoval  48654  itcoval1  48656  itcoval2  48657  itcoval3  48658  itcovalsucov  48661  lines  48724  spheres  48739  discsnterm  49567  termolmd  49663