Theorem elex 3463

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

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

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 3444

This theorem is referenced by:  elexi  3465  elexd  3466  prcnel  3468  spcimgfi1OLD  3507  vtoclgf  3527  vtocl2gf  3529  vtocl3gf  3530  vtocl2g  3531  vtocl3g  3532  spcgv  3552  spc3egv  3559  elab4g  3640  elrabf  3645  elrab  3648  elrab2w  3652  class2seteq  3664  mob  3677  sbcex  3752  sbcel1v  3808  sbcabel  3830  csbiebt  3880  eldif  3913  elin  3919  ssv  3960  elun  4107  csbnestgfw  4376  sbcco3gw  4379  csbnestgf  4381  sbcco3g  4384  csbco3g  4385  csbvarg  4388  sbccsb2  4391  elpwb  4564  pwidb  4577  elpr2g  4608  snidb  4620  ifpr  4652  snssg  4742  eldifvsn  4755  preqsnd  4817  elpreqpr  4825  dfopg  4829  eluni  4868  eliun  4952  csbexg  5257  nvel  5263  axpweq  5298  reusv2lem4  5348  elopab  5483  epelg  5533  opelvvg  5673  opeliunxp2  5795  opelres  5952  imasng  6051  elimasni  6058  iniseg  6064  inisegn0  6065  dmmptg  6208  elon2  6336  ordsssuc2  6418  iota2  6489  fnmptf  6636  fnmpt  6640  fvelimab  6914  mpteqb  6969  fvmptt  6970  fvmptf  6971  fvopab5  6983  fvopab6  6984  fprg  7110  eloprabga  7477  ovmpos  7516  ov2gf  7517  ovmpox  7521  ovmpoga  7522  ovmpt3rab1  7626  brrpssg  7680  sorpssi  7684  unexgOLD  7704  elpwun  7724  ordeleqon  7737  onintrab  7751  sucexg  7760  sucexeloni  7764  ordsucelsuc  7774  onzsl  7798  dmfexALT  7860  elxp5  7875  fabexg  7890  f1oabexg  7894  offval3  7936  releldm2  7997  fnmpo  8023  mpoexg  8030  bropfvvvv  8044  fsplitfpar  8070  suppval  8114  opeliunxp2f  8162  brtpos2  8184  undefval  8228  tfr2b  8337  tz7.49  8386  oeordi  8525  relelec  8693  ecdmn0  8698  mapvalg  8785  pmvalg  8786  elpmg  8792  elixp2  8851  mptelixpg  8885  elixpsn  8887  2pwuninel  9072  ordfin  9152  rex2dom  9165  fival  9327  elfi2  9329  dffi2  9338  elfiun  9345  wemapso2lem  9469  harval  9477  brwdom  9484  fowdom  9488  brwdom2  9490  brwdom3  9499  en2lp  9527  cantnfsuc  9591  rankvalb  9721  rankwflem  9739  rankr1g  9756  r1pwALT  9770  r1rankid  9783  djulcl  9834  djurcl  9835  inlresf  9838  inrresf  9840  djuss  9844  1stinl  9851  2ndinl  9852  1stinr  9853  2ndinr  9854  cardval3  9876  dfac8alem  9951  isacn  9966  numacn  9971  acndom  9973  cardinfima  10019  unialeph  10023  ackbij1lem5  10145  cflm  10172  isf32lem2  10276  isfin1-2  10307  itunifval  10338  numth3  10392  ttukeylem1  10431  cardidg  10470  ondomon  10485  elwina  10609  elina  10610  wuncval  10665  tskmval  10762  eltskm  10766  recmulnq  10887  elnp  10910  elnpi  10911  npomex  10919  elfzp12  13531  seqp1  13951  hashinf  14270  hashxnn0  14274  hashnn0pnf  14277  hashxrcl  14292  prsshashgt1  14345  hashmap  14370  lsw  14499  ccatfval  14508  ccats1alpha  14555  swrdval  14579  pfxval  14609  splval  14686  splcl  14687  revval  14695  reps  14705  s3sndisj  14902  s3iunsndisj  14903  trclfv  14935  relexp0g  14957  relexpsucnnr  14960  relexp1g  14961  limsupcl  15408  limsupval  15409  clim  15429  rlim  15430  hashbcval  16942  isstruct2  17088  setsvalg  17105  setsfun0  17111  setscom  17119  strfvnd  17124  setsid  17146  ressval  17172  ressinbas  17184  restval  17358  pwsval  17418  xpsfrnel2  17497  ismre  17521  oppcval  17648  oppccatf  17663  brssc  17750  rescval  17763  issubc  17771  isfunc  17800  homadm  17976  homacd  17977  uncfval  18169  pltfval  18264  lubfval  18283  glbfval  18296  joinfval  18306  meetfval  18320  p0val  18360  p1val  18361  oduclatb  18442  ipoval  18465  pws0g  18710  frmdval  18788  vrmdfval  18793  efmnd  18807  efmnd2hash  18831  eqgfval  19117  gaid  19240  cntzfval  19261  elsymgbas  19315  symg2hash  19333  pmtrfval  19391  symggen  19411  gexval  19519  lsmfval  19579  pj1fval  19635  frgpval  19699  vrgpfval  19707  dmdprd  19941  dprdw  19953  pws1  20272  pwsmgp  20274  dvdsr  20310  isrngim  20393  rgspnval  20557  rnghmsscmap  20575  rhmsscmap  20604  lssset  20896  lspfval  20936  islbs  21040  sraval  21139  zlmval  21482  psgnevpmb  21554  ocvfval  21633  cssval  21649  thlval  21662  dsmmval  21701  dsmmbase  21702  frlmval  21715  uvcfval  21751  islinds  21776  ltbval  22010  evlsval  22053  coe1fval  22158  evls1fval  22275  matval  22367  oftpos  22408  dmatval  22448  scmatval  22460  smadiadetglem2  22628  cpmat  22665  mat2pmatfval  22679  cpm2mfval  22705  decpmatval0  22720  pm2mpval  22751  chpmatfval  22786  basdif0  22909  tgval  22911  eltg  22913  eltg2  22914  neipeltop  23085  ordtval  23145  islocfin  23473  txval  23520  qtopval  23651  isfbas  23785  isfildlem  23813  fmval  23899  fmf  23901  isfcls  23965  alexsubb  24002  tsmsfbas  24084  ustval  24159  elutop  24189  isusp  24217  ispsmet  24260  ismet  24279  isxmet  24280  blfvalps  24339  metustel  24506  tngval  24595  elpi1  25013  rrxval  25355  q1peqb  26129  ig1pval  26149  taylfval  26334  ulmval  26357  elno  27625  elnoOLD  27626  nosupno  27683  noetalem2  27722  nulslts  27783  oldlim  27895  negsval  28033  elz12s  28480  iscgrg  28596  isismt  28618  legval  28668  ishlg  28686  ishpg  28843  iscgra  28893  isinag  28922  isleag  28931  iseqlg  28951  ttgval  28959  xmstrkgc  28970  cplgr2vpr  29518  vtxdgfval  29553  ewlksfval  29687  wksfval  29695  iswlkg  29699  wwlksnon  29936  wspthsnon  29937  avril1  30550  ispligb  30565  gidval  30600  isvcOLD  30667  0vfval  30694  elunop  31960  rabexgfGS  32586  disjdifprg  32662  disjdifprg2  32663  abfmpunirn  32742  rabfmpunirn  32743  hashgt1  32899  indv  32942  mntoval  33075  tocycval  33202  evpmval  33239  altgnsg  33243  sgnsv  33254  inftmrel  33274  isinftm  33275  resvval  33422  ellpi  33466  idlsrgval  33596  rprmval  33609  dimval  33778  dimvalfi  33779  smatfval  33973  lmatval  33991  ispcmp  34035  qqhval2  34160  rrhval  34174  xrhval  34196  esumc  34229  esumpad  34233  esumpcvgval  34256  ofcfval3  34280  issiga  34290  baselsiga  34293  sigasspw  34294  issgon  34301  isrnsigau  34305  sigagenval  34318  ispisys2  34331  cldssbrsiga  34365  sxval  34368  ismeas  34377  cnmbfm  34441  mbfmcnt  34446  elcarsg  34483  sitmval  34527  eulerpartlemt0  34547  sseqval  34566  sseqmw  34569  sseqp1  34573  orvcval  34636  orvcval4  34639  ballotlemsv  34688  prcinf  35291  satf  35569  satfv1lem  35578  satefv  35630  mrexval  35717  mrsubffval  35723  msubffval  35739  mclsval  35779  eldm3  35977  opelco3  35991  elima4  35992  elfix2  36118  elsingles  36132  fvimage  36145  funpartlem  36158  elaltxp  36191  brcolinear2  36274  ellines  36368  topfneec  36571  topfneec2  36572  fnejoin2  36585  limsucncmpi  36661  findabrcl  36670  weiunse  36684  bj-ififc  36807  elelb  37145  bj-pwvrelb  37146  bj-sngltag  37231  bj-xtagex  37237  bj-elsnb  37309  bj-epelg  37316  bj-evalval  37328  bj-ismoore  37358  bj-ideqg1  37419  bj-ideqg1ALT  37420  bj-elid6  37425  bj-diagval  37429  bj-eldiag2  37432  bj-isrvec  37549  finxpreclem1  37644  finxpreclem3  37648  elghomlem2OLD  38137  isrngo  38148  isdivrngo  38201  br1cnvres  38525  riotasv2d  39333  riotasv3d  39336  lshpset  39354  lsatset  39366  lcvfbr  39396  lflset  39435  lkrfval  39463  lkrval2  39466  islshpkrN  39496  ldualset  39501  cmtfvalN  39586  cvrfval  39644  pats  39661  llnset  39881  lplnset  39905  lvolset  39948  lineset  40114  pointsetN  40117  psubspset  40120  pmapfval  40132  paddfval  40173  pclfvalN  40265  polfvalN  40280  psubclsetN  40312  watfvalN  40368  lhpset  40371  lautset  40458  pautsetN  40474  ldilfset  40484  ltrnfset  40493  dilfsetN  40528  trnfsetN  40531  trlfset  40536  tgrpfset  41120  tendofset  41134  erngfset  41175  erngfset-rN  41183  dvafset  41380  diaffval  41406  dvhfset  41456  docaffvalN  41497  djaffvalN  41509  dibffval  41516  dicffval  41550  dihffval  41606  dochffval  41725  djhffval  41772  lpolsetN  41858  lcdfval  41964  mapdffval  42002  hvmapffval  42134  hdmap1ffval  42171  hdmapffval  42202  hgmapffval  42261  hlhilset  42310  elrfi  43051  nacsfix  43069  mapfzcons2  43076  sbc2rexgOLD  43145  sbc4rexgOLD  43147  setindtrs  43382  wepwso  43400  hbtlem1  43480  hbtlem7  43482  mendval  43536  oaltublim  43647  omord2lim  43657  cnvtrucl0  43980  eliunov2  44035  iunrelexpmin1  44064  iunrelexpmin2  44068  trclfvcom  44079  cnvtrclfv  44080  trclimalb2  44082  trclfvdecomr  44084  gneispacef2  44492  gneispacern2  44495  gneispace0nelrn  44496  addrval  44821  subrval  44822  mulvval  44823  orbitclmpt  45314  elixpconstg  45448  mptfnd  45600  upbdrech  45667  climf  45982  climf2  46024  liminfval  46117  dvcosre  46270  itgsinexplem1  46312  itgsubsticclem  46333  dmvolss  46343  stoweidlem26  46384  stoweidlem35  46393  stirlinglem14  46445  fourierdlem42  46507  fourierdlem81  46545  fourierdlem89  46553  fourierdlem91  46555  salgenval  46679  elsprel  47835  sprval  47839  prprval  47874  isisubgr  48222  isgrim  48242  uhgrimisgrgric  48291  grtri  48300  isgrlim  48342  usgrexmpl2nb0  48391  usgrexmpl2nb1  48392  usgrexmpl2nb3  48394  upwlksfval  48495  isupwlkg  48497  intopval  48562  clintopval  48564  assintopval  48565  rngcvalALTV  48625  ringcvalALTV  48649  dmatbas  48763  lincop  48768  lcoop  48771  fdivval  48899  blenval  48931  itcoval  49021  itcoval1  49023  itcoval2  49024  itcoval3  49025  itcovalsucov  49028  lines  49091  spheres  49106  discsnterm  49933  termolmd  50029