Theorem elex 3457

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

Syntax hints:   → wi 4   = wceq 1541  ∃wex 1780   ∈ wcel 2111  Vcvv 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438

This theorem is referenced by:  elexi  3459  elexd  3460  prcnel  3462  spcimgfi1OLD  3501  vtoclgf  3521  vtocl2gf  3523  vtocl3gf  3524  vtocl2g  3525  vtocl3g  3526  spcgv  3546  spc3egv  3553  elab4g  3634  elrabf  3639  elrab  3642  elrab2w  3646  class2seteq  3658  mob  3671  sbcex  3746  sbcel1v  3802  sbcabel  3824  csbiebt  3874  eldif  3907  elin  3913  ssv  3954  elun  4100  csbnestgfw  4369  sbcco3gw  4372  csbnestgf  4374  sbcco3g  4377  csbco3g  4378  csbvarg  4381  sbccsb2  4384  elpwb  4555  pwidb  4568  elpr2g  4599  snidb  4611  ifpr  4643  snssg  4733  eldifvsn  4746  preqsnd  4808  elpreqpr  4816  dfopg  4820  eluni  4859  eliun  4943  csbexg  5246  nvel  5252  axpweq  5287  reusv2lem4  5337  elopab  5465  epelg  5515  opelvvg  5655  opeliunxp2  5777  opelres  5933  imasng  6032  elimasni  6039  iniseg  6045  inisegn0  6046  dmmptg  6189  elon2  6317  ordsssuc2  6399  iota2  6470  fnmptf  6617  fnmpt  6621  fvelimab  6894  mpteqb  6948  fvmptt  6949  fvmptf  6950  fvopab5  6962  fvopab6  6963  fprg  7088  eloprabga  7455  ovmpos  7494  ov2gf  7495  ovmpox  7499  ovmpoga  7500  ovmpt3rab1  7604  brrpssg  7658  sorpssi  7662  unexgOLD  7682  elpwun  7702  ordeleqon  7715  onintrab  7729  sucexg  7738  sucexeloni  7742  ordsucelsuc  7752  onzsl  7776  dmfexALT  7838  elxp5  7853  fabexg  7868  f1oabexg  7872  offval3  7914  releldm2  7975  fnmpo  8001  mpoexg  8008  bropfvvvv  8022  fsplitfpar  8048  suppval  8092  opeliunxp2f  8140  brtpos2  8162  undefval  8206  tfr2b  8315  tz7.49  8364  oeordi  8502  relelec  8669  ecdmn0  8674  mapvalg  8760  pmvalg  8761  elpmg  8767  elixp2  8825  mptelixpg  8859  elixpsn  8861  2pwuninel  9045  rex2dom  9137  fival  9296  elfi2  9298  dffi2  9307  elfiun  9314  wemapso2lem  9438  harval  9446  brwdom  9453  fowdom  9457  brwdom2  9459  brwdom3  9468  en2lp  9496  cantnfsuc  9560  rankvalb  9690  rankwflem  9708  rankr1g  9725  r1pwALT  9739  r1rankid  9752  djulcl  9803  djurcl  9804  inlresf  9807  inrresf  9809  djuss  9813  1stinl  9820  2ndinl  9821  1stinr  9822  2ndinr  9823  cardval3  9845  dfac8alem  9920  isacn  9935  numacn  9940  acndom  9942  cardinfima  9988  unialeph  9992  ackbij1lem5  10114  cflm  10141  isf32lem2  10245  isfin1-2  10276  itunifval  10307  numth3  10361  ttukeylem1  10400  cardidg  10439  ondomon  10454  elwina  10577  elina  10578  wuncval  10633  tskmval  10730  eltskm  10734  recmulnq  10855  elnp  10878  elnpi  10879  npomex  10887  elfzp12  13503  seqp1  13923  hashinf  14242  hashxnn0  14246  hashnn0pnf  14249  hashxrcl  14264  prsshashgt1  14317  hashmap  14342  lsw  14471  ccatfval  14480  ccats1alpha  14527  swrdval  14551  pfxval  14581  splval  14658  splcl  14659  revval  14667  reps  14677  s3sndisj  14874  s3iunsndisj  14875  trclfv  14907  relexp0g  14929  relexpsucnnr  14932  relexp1g  14933  limsupcl  15380  limsupval  15381  clim  15401  rlim  15402  hashbcval  16914  isstruct2  17060  setsvalg  17077  setsfun0  17083  setscom  17091  strfvnd  17096  setsid  17118  ressval  17144  ressinbas  17156  restval  17330  pwsval  17390  xpsfrnel2  17468  ismre  17492  oppcval  17619  oppccatf  17634  brssc  17721  rescval  17734  issubc  17742  isfunc  17771  homadm  17947  homacd  17948  uncfval  18140  pltfval  18235  lubfval  18254  glbfval  18267  joinfval  18277  meetfval  18291  p0val  18331  p1val  18332  oduclatb  18413  ipoval  18436  pws0g  18681  frmdval  18759  vrmdfval  18764  efmnd  18778  efmnd2hash  18802  eqgfval  19088  gaid  19211  cntzfval  19232  elsymgbas  19286  symg2hash  19304  pmtrfval  19362  symggen  19382  gexval  19490  lsmfval  19550  pj1fval  19606  frgpval  19670  vrgpfval  19678  dmdprd  19912  dprdw  19924  pws1  20243  pwsmgp  20245  dvdsr  20280  isrngim  20363  rgspnval  20527  rnghmsscmap  20545  rhmsscmap  20574  lssset  20866  lspfval  20906  islbs  21010  sraval  21109  zlmval  21452  psgnevpmb  21524  ocvfval  21603  cssval  21619  thlval  21632  dsmmval  21671  dsmmbase  21672  frlmval  21685  uvcfval  21721  islinds  21746  ltbval  21978  evlsval  22021  coe1fval  22118  evls1fval  22234  matval  22326  oftpos  22367  dmatval  22407  scmatval  22419  smadiadetglem2  22587  cpmat  22624  mat2pmatfval  22638  cpm2mfval  22664  decpmatval0  22679  pm2mpval  22710  chpmatfval  22745  basdif0  22868  tgval  22870  eltg  22872  eltg2  22873  neipeltop  23044  ordtval  23104  islocfin  23432  txval  23479  qtopval  23610  isfbas  23744  isfildlem  23772  fmval  23858  fmf  23860  isfcls  23924  alexsubb  23961  tsmsfbas  24043  ustval  24118  elutop  24148  isusp  24176  ispsmet  24219  ismet  24238  isxmet  24239  blfvalps  24298  metustel  24465  tngval  24554  elpi1  24972  rrxval  25314  q1peqb  26088  ig1pval  26108  taylfval  26293  ulmval  26316  elno  27584  elnoOLD  27585  nosupno  27642  noetalem2  27681  oldlim  27832  negsval  27967  elzs12  28383  iscgrg  28490  isismt  28512  legval  28562  ishlg  28580  ishpg  28737  iscgra  28787  isinag  28816  isleag  28825  iseqlg  28845  ttgval  28853  xmstrkgc  28864  cplgr2vpr  29411  vtxdgfval  29446  ewlksfval  29580  wksfval  29588  iswlkg  29592  wwlksnon  29829  wspthsnon  29830  avril1  30443  ispligb  30457  gidval  30492  isvcOLD  30559  0vfval  30586  elunop  31852  rabexgfGS  32479  disjdifprg  32555  disjdifprg2  32556  abfmpunirn  32634  rabfmpunirn  32635  hashgt1  32790  indv  32833  mntoval  32963  tocycval  33077  evpmval  33114  altgnsg  33118  sgnsv  33129  inftmrel  33149  isinftm  33150  resvval  33294  ellpi  33338  idlsrgval  33468  rprmval  33481  dimval  33613  dimvalfi  33614  smatfval  33808  lmatval  33826  ispcmp  33870  qqhval2  33995  rrhval  34009  xrhval  34031  esumc  34064  esumpad  34068  esumpcvgval  34091  ofcfval3  34115  issiga  34125  baselsiga  34128  sigasspw  34129  issgon  34136  isrnsigau  34140  sigagenval  34153  ispisys2  34166  cldssbrsiga  34200  sxval  34203  ismeas  34212  cnmbfm  34276  mbfmcnt  34281  elcarsg  34318  sitmval  34362  eulerpartlemt0  34382  sseqval  34401  sseqmw  34404  sseqp1  34408  orvcval  34471  orvcval4  34474  ballotlemsv  34523  prcinf  35136  satf  35397  satfv1lem  35406  satefv  35458  mrexval  35545  mrsubffval  35551  msubffval  35567  mclsval  35607  eldm3  35805  opelco3  35819  elima4  35820  elfix2  35946  elsingles  35960  fvimage  35973  funpartlem  35986  elaltxp  36019  brcolinear2  36102  ellines  36196  topfneec  36399  topfneec2  36400  fnejoin2  36413  limsucncmpi  36489  findabrcl  36498  weiunse  36512  bj-ififc  36626  elelb  36941  bj-pwvrelb  36942  bj-sngltag  37027  bj-xtagex  37033  bj-elsnb  37105  bj-epelg  37112  bj-evalval  37119  bj-ismoore  37149  bj-ideqg1  37208  bj-ideqg1ALT  37209  bj-elid6  37214  bj-diagval  37218  bj-eldiag2  37221  bj-isrvec  37338  finxpreclem1  37433  finxpreclem3  37437  elghomlem2OLD  37936  isrngo  37947  isdivrngo  38000  br1cnvres  38316  riotasv2d  39066  riotasv3d  39069  lshpset  39087  lsatset  39099  lcvfbr  39129  lflset  39168  lkrfval  39196  lkrval2  39199  islshpkrN  39229  ldualset  39234  cmtfvalN  39319  cvrfval  39377  pats  39394  llnset  39614  lplnset  39638  lvolset  39681  lineset  39847  pointsetN  39850  psubspset  39853  pmapfval  39865  paddfval  39906  pclfvalN  39998  polfvalN  40013  psubclsetN  40045  watfvalN  40101  lhpset  40104  lautset  40191  pautsetN  40207  ldilfset  40217  ltrnfset  40226  dilfsetN  40261  trnfsetN  40264  trlfset  40269  tgrpfset  40853  tendofset  40867  erngfset  40908  erngfset-rN  40916  dvafset  41113  diaffval  41139  dvhfset  41189  docaffvalN  41230  djaffvalN  41242  dibffval  41249  dicffval  41283  dihffval  41339  dochffval  41458  djhffval  41505  lpolsetN  41591  lcdfval  41697  mapdffval  41735  hvmapffval  41867  hdmap1ffval  41904  hdmapffval  41935  hgmapffval  41994  hlhilset  42043  elrfi  42797  nacsfix  42815  mapfzcons2  42822  sbc2rexgOLD  42891  sbc4rexgOLD  42893  setindtrs  43128  wepwso  43146  hbtlem1  43226  hbtlem7  43228  mendval  43282  oaltublim  43393  omord2lim  43403  cnvtrucl0  43727  eliunov2  43782  iunrelexpmin1  43811  iunrelexpmin2  43815  trclfvcom  43826  cnvtrclfv  43827  trclimalb2  43829  trclfvdecomr  43831  gneispacef2  44239  gneispacern2  44242  gneispace0nelrn  44243  addrval  44568  subrval  44569  mulvval  44570  orbitclmpt  45061  elixpconstg  45196  mptfnd  45349  upbdrech  45416  climf  45732  climf2  45774  liminfval  45867  dvcosre  46020  itgsinexplem1  46062  itgsubsticclem  46083  dmvolss  46093  stoweidlem26  46134  stoweidlem35  46143  stirlinglem14  46195  fourierdlem42  46257  fourierdlem81  46295  fourierdlem89  46303  fourierdlem91  46305  salgenval  46429  elsprel  47585  sprval  47589  prprval  47624  isisubgr  47972  isgrim  47992  uhgrimisgrgric  48041  grtri  48050  isgrlim  48092  usgrexmpl2nb0  48141  usgrexmpl2nb1  48142  usgrexmpl2nb3  48144  upwlksfval  48245  isupwlkg  48247  intopval  48312  clintopval  48314  assintopval  48315  rngcvalALTV  48375  ringcvalALTV  48399  dmatbas  48514  lincop  48519  lcoop  48522  fdivval  48650  blenval  48682  itcoval  48772  itcoval1  48774  itcoval2  48775  itcoval3  48776  itcovalsucov  48779  lines  48842  spheres  48857  discsnterm  49685  termolmd  49781