Theorem elex 3484

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

Syntax hints:   → wi 4   = wceq 1567  ∃wex 1806   ∈ wcel 2149  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465

This theorem is referenced by:  elexi  3485  elexd  3486  prcnel  3488  spcimgfi1OLD  3525  vtoclgf  3543  vtocl2gf  3545  vtocl3gf  3546  vtocl2g  3547  vtocl3g  3548  spcgv  3564  spc3egv  3571  elab4g  3651  elrabf  3656  elrab  3659  elrab2w  3664  class2seteq  3676  mob  3689  sbcex  3763  sbcel1v  3818  sbcabel  3840  csbiebt  3890  eldif  3923  elin  3929  ssv  3969  elun  4115  csbnestgfw  4393  sbcco3gw  4396  csbnestgf  4398  sbcco3g  4401  csbco3g  4402  csbvarg  4405  sbccsb2  4408  elpwb  4575  pwidg  4587  pwidb  4589  elpr2g  4620  snidb  4632  ifpr  4664  snssg  4754  eldifvsn  4769  preqsnd  4828  elpreqpr  4836  dfopg  4840  eluni  4879  eliun  4964  csbexg  5275  nvelOLD  5287  axpweq  5322  reusv2lem4  5373  elopab  5512  epelg  5563  opelvvg  5703  opeliunxp2  5825  opelres  5985  imasng  6087  elimasni  6094  iniseg  6100  inisegn0  6101  dmmptg  6244  elon2  6372  ordsssuc2  6455  iota2  6526  fnmptf  6672  fnmpt  6676  fvelimab  6954  mpteqb  7010  fvmptt  7011  fvmptf  7012  fvopab5  7024  fvopab6  7025  fprg  7153  eloprabga  7520  ovmpos  7559  ov2gf  7560  ovmpox  7564  ovmpoga  7565  ovmpt3rab1  7669  brrpssg  7723  sorpssi  7727  unexgOLD  7748  elpwun  7768  ordeleqon  7781  onintrab  7795  sucexg  7804  sucexeloni  7808  ordsucelsuc  7818  onzsl  7842  dmfexALT  7905  elxp5  7920  fabexg  7935  f1oabexg  7938  offval3  7979  releldm2  8040  fnmpo  8066  mpoexg  8073  bropfvvvv  8087  fsplitfpar  8113  suppval  8158  opeliunxp2f  8206  brtpos2  8228  undefval  8273  tfr2b  8383  tz7.49  8432  oeordi  8573  relelec  8742  ecdmn0  8747  mapvalg  8833  pmvalg  8834  elpmg  8840  elixp2  8899  mptelixpg  8933  elixpsn  8935  2pwuninel  9120  ordfin  9200  rex2dom  9213  fival  9372  elfi2  9374  dffi2  9383  elfiun  9390  wemapso2lem  9514  harval  9522  brwdom  9529  fowdom  9533  brwdom2  9535  brwdom3  9544  en2lp  9575  cantnfsuc  9639  rankvalb  9769  rankwflem  9787  rankr1g  9804  r1pwALT  9818  r1rankid  9831  djulcl  9896  djurcl  9897  inlresf  9900  inrresf  9902  djuss  9906  1stinl  9913  2ndinl  9914  1stinr  9915  2ndinr  9916  cardval3  9938  dfac8alem  10013  isacn  10028  numacn  10033  acndom  10035  cardinfima  10081  unialeph  10085  ackbij1lem5  10206  cflm  10233  isf32lem2  10338  isfin1-2  10369  itunifval  10400  numth3  10454  ttukeylem1  10493  cardidg  10532  ondomon  10547  elwina  10671  elina  10672  wuncval  10727  tskmval  10824  eltskm  10828  recmulnq  10949  elnp  10972  elnpi  10973  npomex  10981  indv  12220  elfzp12  13631  seqp1  14052  hashinf  14371  hashxnn0  14375  hashnn0pnf  14378  hashxrcl  14393  prsshashgt1  14447  hashmap  14472  lsw  14601  ccatfval  14610  ccats1alpha  14657  swrdval  14681  pfxval  14711  splval  14788  splcl  14789  revval  14797  reps  14807  s3sndisj  15004  s3iunsndisj  15005  trclfv  15037  relexp0g  15059  relexpsucnnr  15062  relexp1g  15063  limsupcl  15524  limsupval  15525  clim  15545  rlim  15546  hashbcval  17062  isstruct2  17209  setsvalg  17226  setsfun0  17232  setscom  17240  strfvnd  17245  setsid  17267  ressval  17293  ressinbas  17305  restval  17479  pwsval  17539  xpsfrnel2  17618  ismre  17642  oppcval  17769  oppccatf  17784  brssc  17871  rescval  17884  issubc  17892  isfunc  17921  homadm  18097  homacd  18098  uncfval  18290  pltfval  18385  lubfval  18404  glbfval  18417  joinfval  18427  meetfval  18441  p0val  18481  p1val  18482  oduclatb  18563  ipoval  18586  pws0g  18831  frmdval  18910  vrmdfval  18915  efmnd  18929  efmnd2hash  18953  eqgfval  19244  gaid  19369  cntzfval  19390  elsymgbas  19444  symg2hash  19462  pmtrfval  19520  symggen  19540  gexval  19648  lsmfval  19708  pj1fval  19764  frgpval  19828  vrgpfval  19836  dmdprd  20070  dprdw  20082  pws1  20406  pwsmgp  20408  dvdsr  20444  isrngim  20527  rgspnval  20697  rnghmsscmap  20715  rhmsscmap  20744  lssset  21032  lspfval  21072  islbs  21175  sraval  21274  zlmval  21634  psgnevpmb  21706  ocvfval  21785  cssval  21801  thlval  21814  dsmmval  21853  dsmmbase  21854  frlmval  21867  uvcfval  21903  islinds  21928  ltbval  22163  evlsval  22206  coe1fval  22334  evls1fval  22448  matval  22537  oftpos  22578  dmatval  22618  scmatval  22630  smadiadetglem2  22798  cpmat  22835  mat2pmatfval  22849  cpm2mfval  22875  decpmatval0  22890  pm2mpval  22921  chpmatfval  22956  basdif0  23079  tgval  23081  eltg  23083  eltg2  23084  neipeltop  23255  ordtval  23315  islocfin  23643  txval  23690  qtopval  23821  isfbas  23955  isfildlem  23983  fmval  24069  fmf  24071  isfcls  24135  alexsubb  24172  tsmsfbas  24254  ustval  24329  elutop  24359  isusp  24387  ispsmet  24430  ismet  24449  isxmet  24450  blfvalps  24509  metustel  24676  tngval  24765  elpi1  25173  rrxval  25515  q1peqb  26282  ig1pval  26302  taylfval  26488  ulmval  26509  elno  27776  nosupno  27833  noetalem2  27872  nulslts  27934  oldlim  28046  negsval  28184  elz12s  28631  iscgrg  28747  isismt  28769  legval  28819  ishlg  28837  ishpg  29000  iscgra  29077  isinag  29110  isleag  29119  iseqlg  29139  ttgval  29165  xmstrkgc  29176  cplgr2vpr  29724  vtxdgfval  29758  ewlksfval  29892  wksfval  29900  iswlkg  29904  wwlksnon  30141  wspthsnon  30142  avril1  30755  ispligb  30770  gidval  30805  isvcOLD  30872  0vfval  30899  elunop  32165  rabexgfGS  32786  disjdifprg  32861  disjdifprg2  32862  abfmpunirn  32938  rabfmpunirn  32939  hashgt1  33094  mntoval  33243  tocycval  33369  evpmval  33406  altgnsg  33410  sgnsv  33421  inftmrel  33441  isinftm  33442  resvval  33592  ellpi  33630  idlsrgval  33738  rprmval  33751  dimval  33936  dimvalfi  33937  smatfval  34130  lmatval  34148  ispcmp  34192  qqhval2  34317  rrhval  34331  xrhval  34353  esumc  34386  esumpad  34390  esumpcvgval  34413  ofcfval3  34437  issiga  34447  baselsiga  34450  sigasspw  34451  issgon  34458  isrnsigau  34462  sigagenval  34475  ispisys2  34488  cldssbrsiga  34522  sxval  34525  ismeas  34534  cnmbfm  34598  mbfmcnt  34603  elcarsg  34640  sitmval  34684  eulerpartlemt0  34704  sseqval  34723  sseqmw  34726  sseqp1  34730  orvcval  34793  orvcval4  34796  ballotlemsv  34845  acnum  35458  prcinf  35459  satf  35778  satfv1lem  35787  satefv  35839  mrexval  35926  mrsubffval  35932  msubffval  35948  mclsval  35988  eldm3  36186  opelco3  36200  elima4  36201  elfix2  36327  elsingles  36341  fvimage  36354  funpartlem  36367  elaltxp  36400  brcolinear2  36483  ellines  36577  topfneec  36789  topfneec2  36790  fnejoin2  36803  limsucncmpi  36879  findabrcl  36888  weiunse  36902  ttcwf2  36959  bj-ififc  37098  elelb  37455  bj-pwvrelb  37456  bj-sngltag  37541  bj-xtagex  37547  bj-elsnb  37619  bj-epelg  37626  bj-evalval  37639  bj-ismoore  37669  bj-ideqg1  37730  bj-ideqg1ALT  37731  bj-elid6  37736  bj-diagval  37740  bj-eldiag2  37743  bj-isrvec  37860  finxpreclem1  37957  finxpreclem3  37961  elghomlem2OLD  38459  isrngo  38470  isdivrngo  38523  br1cnvres  38847  riotasv2d  39655  riotasv3d  39658  lshpset  39676  lsatset  39688  lcvfbr  39718  lflset  39757  lkrfval  39785  lkrval2  39788  islshpkrN  39818  ldualset  39823  cmtfvalN  39908  cvrfval  39966  pats  39983  llnset  40203  lplnset  40227  lvolset  40270  lineset  40436  pointsetN  40439  psubspset  40442  pmapfval  40454  paddfval  40495  pclfvalN  40587  polfvalN  40602  psubclsetN  40634  watfvalN  40690  lhpset  40693  lautset  40780  pautsetN  40796  ldilfset  40806  ltrnfset  40815  dilfsetN  40850  trnfsetN  40853  trlfset  40858  tgrpfset  41442  tendofset  41456  erngfset  41497  erngfset-rN  41505  dvafset  41702  diaffval  41728  dvhfset  41778  docaffvalN  41819  djaffvalN  41831  dibffval  41838  dicffval  41872  dihffval  41928  dochffval  42047  djhffval  42094  lpolsetN  42180  lcdfval  42286  mapdffval  42324  hvmapffval  42456  hdmap1ffval  42493  hdmapffval  42524  hgmapffval  42583  hlhilset  42632  elrfi  43351  nacsfix  43369  mapfzcons2  43376  setindtrs  43678  wepwso  43696  hbtlem1  43776  hbtlem7  43778  mendval  43832  oaltublim  43943  omord2lim  43953  cnvtrucl0  44276  eliunov2  44331  iunrelexpmin1  44360  iunrelexpmin2  44364  trclfvcom  44375  cnvtrclfv  44376  trclimalb2  44378  trclfvdecomr  44380  gneispacef2  44788  gneispacern2  44791  gneispace0nelrn  44792  addrval  45100  subrval  45101  mulvval  45102  orbitclmpt  45593  elixpconstg  45733  mptfnd  45883  upbdrech  45950  climf  46264  climf2  46306  liminfval  46399  dvcosre  46552  itgsinexplem1  46594  itgsubsticclem  46615  dmvolss  46625  stoweidlem26  46666  stoweidlem35  46675  stirlinglem14  46727  fourierdlem42  46789  fourierdlem81  46827  fourierdlem89  46835  fourierdlem91  46837  salgenval  46961  elsprel  48147  sprval  48151  prprval  48186  isisubgr  48550  isgrim  48570  uhgrimisgrgric  48619  grtri  48628  isgrlim  48670  usgrexmpl2nb0  48719  usgrexmpl2nb1  48720  usgrexmpl2nb3  48722  upwlksfval  48823  isupwlkg  48825  intopval  48890  clintopval  48892  assintopval  48893  rngcvalALTV  48953  ringcvalALTV  48977  dmatbas  49102  lincop  49107  lcoop  49110  fdivval  49238  blenval  49270  itcoval  49360  itcoval1  49362  itcoval2  49363  itcoval3  49364  itcovalsucov  49367  lines  49430  spheres  49445  discsnterm  50271  termolmd  50367