Theorem elex 3475

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

Syntax hints:   → wi 4   = wceq 1560  ∃wex 1799   ∈ wcel 2142  Vcvv 3454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456

This theorem is referenced by:  elexi  3476  elexd  3477  prcnel  3479  spcimgfi1OLD  3516  vtoclgf  3534  vtocl2gf  3536  vtocl3gf  3537  vtocl2g  3538  vtocl3g  3539  spcgv  3555  spc3egv  3562  elab4g  3642  elrabf  3647  elrab  3650  elrab2w  3655  class2seteq  3667  mob  3680  sbcex  3754  sbcel1v  3809  sbcabel  3831  csbiebt  3881  eldif  3914  elin  3920  ssv  3960  elun  4106  csbnestgfw  4376  sbcco3gw  4379  csbnestgf  4381  sbcco3g  4384  csbco3g  4385  csbvarg  4388  sbccsb2  4391  elpwb  4563  pwidg  4575  pwidb  4577  elpr2g  4608  snidb  4620  ifpr  4652  snssg  4742  eldifvsn  4757  preqsnd  4817  elpreqpr  4825  dfopg  4829  eluni  4868  eliun  4953  csbexg  5260  nvelOLD  5272  axpweq  5307  reusv2lem4  5358  elopab  5497  epelg  5548  opelvvg  5688  opeliunxp2  5810  opelres  5971  imasng  6073  elimasni  6080  iniseg  6086  inisegn0  6087  dmmptg  6229  elon2  6357  ordsssuc2  6439  iota2  6510  fnmptf  6657  fnmpt  6661  fvelimab  6939  mpteqb  6995  fvmptt  6996  fvmptf  6997  fvopab5  7009  fvopab6  7010  fprg  7138  eloprabga  7505  ovmpos  7544  ov2gf  7545  ovmpox  7549  ovmpoga  7550  ovmpt3rab1  7654  brrpssg  7708  sorpssi  7712  unexgOLD  7732  elpwun  7752  ordeleqon  7765  onintrab  7779  sucexg  7788  sucexeloni  7792  ordsucelsuc  7802  onzsl  7826  dmfexALT  7889  elxp5  7904  fabexg  7919  f1oabexg  7922  offval3  7963  releldm2  8024  fnmpo  8050  mpoexg  8057  bropfvvvv  8071  fsplitfpar  8097  suppval  8142  opeliunxp2f  8190  brtpos2  8212  undefval  8257  tfr2b  8367  tz7.49  8416  oeordi  8557  relelec  8726  ecdmn0  8731  mapvalg  8817  pmvalg  8818  elpmg  8824  elixp2  8883  mptelixpg  8917  elixpsn  8919  2pwuninel  9104  ordfin  9184  rex2dom  9197  fival  9358  elfi2  9360  dffi2  9369  elfiun  9376  wemapso2lem  9500  harval  9508  brwdom  9515  fowdom  9519  brwdom2  9521  brwdom3  9530  en2lp  9561  cantnfsuc  9625  rankvalb  9755  rankwflem  9773  rankr1g  9790  r1pwALT  9804  r1rankid  9817  djulcl  9868  djurcl  9869  inlresf  9872  inrresf  9874  djuss  9878  1stinl  9885  2ndinl  9886  1stinr  9887  2ndinr  9888  cardval3  9910  dfac8alem  9985  isacn  10000  numacn  10005  acndom  10007  cardinfima  10053  unialeph  10057  ackbij1lem5  10179  cflm  10206  isf32lem2  10311  isfin1-2  10342  itunifval  10373  numth3  10427  ttukeylem1  10466  cardidg  10505  ondomon  10520  elwina  10644  elina  10645  wuncval  10700  tskmval  10797  eltskm  10801  recmulnq  10922  elnp  10945  elnpi  10946  npomex  10954  indv  12197  elfzp12  13608  seqp1  14029  hashinf  14348  hashxnn0  14352  hashnn0pnf  14355  hashxrcl  14370  prsshashgt1  14423  hashmap  14448  lsw  14577  ccatfval  14586  ccats1alpha  14633  swrdval  14657  pfxval  14687  splval  14764  splcl  14765  revval  14773  reps  14783  s3sndisj  14980  s3iunsndisj  14981  trclfv  15013  relexp0g  15035  relexpsucnnr  15038  relexp1g  15039  limsupcl  15500  limsupval  15501  clim  15521  rlim  15522  hashbcval  17038  isstruct2  17185  setsvalg  17202  setsfun0  17208  setscom  17216  strfvnd  17221  setsid  17243  ressval  17269  ressinbas  17281  restval  17455  pwsval  17515  xpsfrnel2  17594  ismre  17618  oppcval  17745  oppccatf  17760  brssc  17847  rescval  17860  issubc  17868  isfunc  17897  homadm  18073  homacd  18074  uncfval  18266  pltfval  18361  lubfval  18380  glbfval  18393  joinfval  18403  meetfval  18417  p0val  18457  p1val  18458  oduclatb  18539  ipoval  18562  pws0g  18807  frmdval  18885  vrmdfval  18890  efmnd  18904  efmnd2hash  18928  eqgfval  19217  gaid  19339  cntzfval  19360  elsymgbas  19414  symg2hash  19432  pmtrfval  19490  symggen  19510  gexval  19618  lsmfval  19678  pj1fval  19734  frgpval  19798  vrgpfval  19806  dmdprd  20040  dprdw  20052  pws1  20373  pwsmgp  20375  dvdsr  20411  isrngim  20494  rgspnval  20662  rnghmsscmap  20680  rhmsscmap  20709  lssset  21000  lspfval  21040  islbs  21143  sraval  21242  zlmval  21567  psgnevpmb  21639  ocvfval  21718  cssval  21734  thlval  21747  dsmmval  21786  dsmmbase  21787  frlmval  21800  uvcfval  21836  islinds  21861  ltbval  22096  evlsval  22139  coe1fval  22267  evls1fval  22382  matval  22471  oftpos  22512  dmatval  22552  scmatval  22564  smadiadetglem2  22732  cpmat  22769  mat2pmatfval  22783  cpm2mfval  22809  decpmatval0  22824  pm2mpval  22855  chpmatfval  22890  basdif0  23013  tgval  23015  eltg  23017  eltg2  23018  neipeltop  23189  ordtval  23249  islocfin  23577  txval  23624  qtopval  23755  isfbas  23889  isfildlem  23917  fmval  24003  fmf  24005  isfcls  24069  alexsubb  24106  tsmsfbas  24188  ustval  24263  elutop  24293  isusp  24321  ispsmet  24364  ismet  24383  isxmet  24384  blfvalps  24443  metustel  24610  tngval  24699  elpi1  25107  rrxval  25449  q1peqb  26216  ig1pval  26236  taylfval  26422  ulmval  26443  elno  27710  nosupno  27767  noetalem2  27806  nulslts  27868  oldlim  27980  negsval  28118  elz12s  28565  iscgrg  28681  isismt  28703  legval  28753  ishlg  28771  ishpg  28932  iscgra  29003  isinag  29032  isleag  29041  iseqlg  29061  ttgval  29075  xmstrkgc  29086  cplgr2vpr  29634  vtxdgfval  29668  ewlksfval  29802  wksfval  29810  iswlkg  29814  wwlksnon  30051  wspthsnon  30052  avril1  30665  ispligb  30680  gidval  30715  isvcOLD  30782  0vfval  30809  elunop  32075  rabexgfGS  32698  disjdifprg  32775  disjdifprg2  32776  abfmpunirn  32854  rabfmpunirn  32855  hashgt1  33010  mntoval  33160  tocycval  33288  evpmval  33325  altgnsg  33329  sgnsv  33340  inftmrel  33360  isinftm  33361  resvval  33515  ellpi  33559  idlsrgval  33699  rprmval  33712  dimval  33898  dimvalfi  33899  smatfval  34092  lmatval  34110  ispcmp  34154  qqhval2  34279  rrhval  34293  xrhval  34315  esumc  34348  esumpad  34352  esumpcvgval  34375  ofcfval3  34399  issiga  34409  baselsiga  34412  sigasspw  34413  issgon  34420  isrnsigau  34424  sigagenval  34437  ispisys2  34450  cldssbrsiga  34484  sxval  34487  ismeas  34496  cnmbfm  34560  mbfmcnt  34565  elcarsg  34602  sitmval  34646  eulerpartlemt0  34666  sseqval  34685  sseqmw  34688  sseqp1  34692  orvcval  34755  orvcval4  34758  ballotlemsv  34807  prcinf  35409  satf  35703  satfv1lem  35712  satefv  35764  mrexval  35851  mrsubffval  35857  msubffval  35873  mclsval  35913  eldm3  36111  opelco3  36125  elima4  36126  elfix2  36252  elsingles  36266  fvimage  36279  funpartlem  36292  elaltxp  36325  brcolinear2  36408  ellines  36502  topfneec  36715  topfneec2  36716  fnejoin2  36729  limsucncmpi  36805  findabrcl  36814  weiunse  36828  ttcwf2  36885  bj-ififc  37025  elelb  37382  bj-pwvrelb  37383  bj-sngltag  37468  bj-xtagex  37474  bj-elsnb  37546  bj-epelg  37553  bj-evalval  37565  bj-ismoore  37595  bj-ideqg1  37656  bj-ideqg1ALT  37657  bj-elid6  37662  bj-diagval  37666  bj-eldiag2  37669  bj-isrvec  37786  finxpreclem1  37883  finxpreclem3  37887  elghomlem2OLD  38385  isrngo  38396  isdivrngo  38449  br1cnvres  38773  riotasv2d  39581  riotasv3d  39584  lshpset  39602  lsatset  39614  lcvfbr  39644  lflset  39683  lkrfval  39711  lkrval2  39714  islshpkrN  39744  ldualset  39749  cmtfvalN  39834  cvrfval  39892  pats  39909  llnset  40129  lplnset  40153  lvolset  40196  lineset  40362  pointsetN  40365  psubspset  40368  pmapfval  40380  paddfval  40421  pclfvalN  40513  polfvalN  40528  psubclsetN  40560  watfvalN  40616  lhpset  40619  lautset  40706  pautsetN  40722  ldilfset  40732  ltrnfset  40741  dilfsetN  40776  trnfsetN  40779  trlfset  40784  tgrpfset  41368  tendofset  41382  erngfset  41423  erngfset-rN  41431  dvafset  41628  diaffval  41654  dvhfset  41704  docaffvalN  41745  djaffvalN  41757  dibffval  41764  dicffval  41798  dihffval  41854  dochffval  41973  djhffval  42020  lpolsetN  42106  lcdfval  42212  mapdffval  42250  hvmapffval  42382  hdmap1ffval  42419  hdmapffval  42450  hgmapffval  42509  hlhilset  42558  elrfi  43275  nacsfix  43293  mapfzcons2  43300  setindtrs  43602  wepwso  43620  hbtlem1  43700  hbtlem7  43702  mendval  43756  oaltublim  43867  omord2lim  43877  cnvtrucl0  44200  eliunov2  44255  iunrelexpmin1  44284  iunrelexpmin2  44288  trclfvcom  44299  cnvtrclfv  44300  trclimalb2  44302  trclfvdecomr  44304  gneispacef2  44712  gneispacern2  44715  gneispace0nelrn  44716  addrval  45041  subrval  45042  mulvval  45043  orbitclmpt  45534  elixpconstg  45667  mptfnd  45817  upbdrech  45884  climf  46198  climf2  46240  liminfval  46333  dvcosre  46486  itgsinexplem1  46528  itgsubsticclem  46549  dmvolss  46559  stoweidlem26  46600  stoweidlem35  46609  stirlinglem14  46661  fourierdlem42  46723  fourierdlem81  46761  fourierdlem89  46769  fourierdlem91  46771  salgenval  46895  elsprel  48081  sprval  48085  prprval  48120  isisubgr  48484  isgrim  48504  uhgrimisgrgric  48553  grtri  48562  isgrlim  48604  usgrexmpl2nb0  48653  usgrexmpl2nb1  48654  usgrexmpl2nb3  48656  upwlksfval  48757  isupwlkg  48759  intopval  48824  clintopval  48826  assintopval  48827  rngcvalALTV  48887  ringcvalALTV  48911  dmatbas  49025  lincop  49030  lcoop  49033  fdivval  49161  blenval  49193  itcoval  49283  itcoval1  49285  itcoval2  49286  itcoval3  49287  itcovalsucov  49290  lines  49353  spheres  49368  discsnterm  50195  termolmd  50291