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

Syntax hints:   → wi 4   = wceq 1539  ∃wex 1778   ∈ wcel 2107  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465

This theorem is referenced by:  elexi  3486  elexd  3487  prcnel  3490  spcimgfi1OLD  3531  vtoclgf  3552  vtocl2gf  3555  vtocl3gf  3556  vtocl2g  3557  vtocl3g  3558  spcgv  3579  spc3egv  3586  elab4g  3666  elrabf  3671  elrab  3675  elrab2w  3679  class2seteq  3692  mob  3705  sbcex  3780  sbcel1v  3836  sbcabel  3858  csbiebt  3908  eldif  3941  elin  3947  ssv  3988  elun  4133  csbnestgfw  4402  sbcco3gw  4405  csbnestgf  4407  sbcco3g  4410  csbco3g  4411  csbvarg  4414  sbccsb2  4417  elpwb  4588  pwidb  4601  elpr2g  4631  snidb  4641  ifpr  4673  snssg  4763  eldifvsn  4777  preqsnd  4839  elpreqpr  4847  dfopg  4851  eluni  4890  eliun  4975  csbexg  5290  nvel  5296  axpweq  5331  reusv2lem4  5381  elopab  5512  epelg  5565  opelvvg  5706  opeliunxp2  5829  opelres  5983  imasng  6082  elimasni  6089  iniseg  6095  inisegn0  6096  dmmptg  6242  elon2  6374  ordsssuc2  6455  iota2  6530  fnmptf  6684  fnmpt  6688  fvelimab  6961  mpteqb  7015  fvmptt  7016  fvmptf  7017  fvopab5  7029  fvopab6  7030  fprg  7155  eloprabga  7524  ovmpos  7563  ov2gf  7564  ovmpox  7568  ovmpoga  7569  ovmpt3rab1  7673  brrpssg  7727  sorpssi  7731  unexgOLD  7751  elpwun  7771  ordeleqon  7784  onintrab  7798  sucexg  7807  sucexeloni  7811  ordsucelsuc  7824  onzsl  7849  dmfexALT  7912  elxp5  7927  fabexg  7942  f1oabexg  7946  offval3  7989  releldm2  8050  fnmpo  8076  mpoexg  8083  mptmpoopabbrdOLDOLD  8090  bropfvvvv  8099  fsplitfpar  8125  suppval  8169  opeliunxp2f  8217  brtpos2  8239  undefval  8283  tfr2b  8418  tz7.49  8467  oeordi  8607  relelec  8774  ecdmn0  8776  mapvalg  8858  pmvalg  8859  elpmg  8865  elixp2  8923  mptelixpg  8957  elixpsn  8959  2pwuninel  9154  rex2dom  9264  fival  9434  elfi2  9436  dffi2  9445  elfiun  9452  wemapso2lem  9574  harval  9582  brwdom  9589  fowdom  9593  brwdom2  9595  brwdom3  9604  en2lp  9628  cantnfsuc  9692  rankvalb  9819  rankwflem  9837  rankr1g  9854  r1pwALT  9868  r1rankid  9881  djulcl  9932  djurcl  9933  inlresf  9936  inrresf  9938  djuss  9942  1stinl  9949  2ndinl  9950  1stinr  9951  2ndinr  9952  cardval3  9974  dfac8alem  10051  isacn  10066  numacn  10071  acndom  10073  cardinfima  10119  unialeph  10123  ackbij1lem5  10245  cflm  10272  isf32lem2  10376  isfin1-2  10407  itunifval  10438  numth3  10492  ttukeylem1  10531  cardidg  10570  ondomon  10585  elwina  10708  elina  10709  wuncval  10764  tskmval  10861  eltskm  10865  recmulnq  10986  elnp  11009  elnpi  11010  npomex  11018  elfzp12  13625  seqp1  14039  hashinf  14357  hashxnn0  14361  hashnn0pnf  14364  hashxrcl  14379  prsshashgt1  14432  hashmap  14457  lsw  14585  ccatfval  14594  ccats1alpha  14640  swrdval  14664  pfxval  14694  splval  14772  splcl  14773  revval  14781  reps  14791  s3sndisj  14989  s3iunsndisj  14990  trclfv  15022  relexp0g  15044  relexpsucnnr  15047  relexp1g  15048  limsupcl  15492  limsupval  15493  clim  15513  rlim  15514  hashbcval  17023  isstruct2  17169  setsvalg  17186  setsfun0  17192  setscom  17200  strfvnd  17205  setsid  17227  ressval  17256  ressinbas  17269  restval  17443  pwsval  17503  xpsfrnel2  17581  ismre  17605  oppcval  17728  oppccatf  17743  brssc  17830  rescval  17843  issubc  17852  isfunc  17881  homadm  18057  homacd  18058  uncfval  18250  pltfval  18346  lubfval  18365  glbfval  18378  joinfval  18388  meetfval  18402  p0val  18442  p1val  18443  oduclatb  18522  ipoval  18545  pws0g  18756  frmdval  18834  vrmdfval  18839  efmnd  18853  efmnd2hash  18877  eqgfval  19164  gaid  19287  cntzfval  19308  elsymgbas  19360  symg2hash  19378  pmtrfval  19437  symggen  19457  gexval  19565  lsmfval  19625  pj1fval  19681  frgpval  19745  vrgpfval  19753  dmdprd  19987  dprdw  19999  pws1  20291  pwsmgp  20293  dvdsr  20331  isrngim  20414  isrim0OLD  20450  rgspnval  20581  rnghmsscmap  20599  rhmsscmap  20628  lssset  20900  lspfval  20940  islbs  21044  sraval  21143  zlmval  21489  psgnevpmb  21560  ocvfval  21639  cssval  21655  thlval  21668  dsmmval  21709  dsmmbase  21710  frlmval  21723  uvcfval  21759  islinds  21784  ltbval  22016  evlsval  22059  coe1fval  22156  evls1fval  22272  matval  22364  oftpos  22407  dmatval  22447  scmatval  22459  smadiadetglem2  22627  cpmat  22664  mat2pmatfval  22678  cpm2mfval  22704  decpmatval0  22719  pm2mpval  22750  chpmatfval  22785  basdif0  22908  tgval  22910  eltg  22912  eltg2  22913  neipeltop  23084  ordtval  23144  islocfin  23472  txval  23519  qtopval  23650  isfbas  23784  isfildlem  23812  fmval  23898  fmf  23900  isfcls  23964  alexsubb  24001  tsmsfbas  24083  ustval  24158  elutop  24189  isusp  24217  ispsmet  24260  ismet  24279  isxmet  24280  blfvalps  24339  metustel  24508  tngval  24597  elpi1  25015  rrxval  25358  q1peqb  26132  ig1pval  26152  taylfval  26337  ulmval  26360  elno  27627  elnoOLD  27628  nosupno  27685  noetalem2  27724  oldlim  27862  negsval  27994  elzs12  28358  iscgrg  28457  isismt  28479  legval  28529  ishlg  28547  ishpg  28704  iscgra  28754  isinag  28783  isleag  28792  iseqlg  28812  ttgval  28820  ttgvalOLD  28821  xmstrkgc  28832  cplgr2vpr  29379  vtxdgfval  29414  ewlksfval  29548  wksfval  29556  iswlkg  29560  wwlksnon  29800  wspthsnon  29801  avril1  30411  ispligb  30425  gidval  30460  isvcOLD  30527  0vfval  30554  elunop  31820  rabexgfGS  32447  disjdifprg  32524  disjdifprg2  32525  abfmpunirn  32598  rabfmpunirn  32599  hashgt1  32756  indv  32782  mntoval  32916  tocycval  33072  evpmval  33109  altgnsg  33113  sgnsv  33124  inftmrel  33131  isinftm  33132  resvval  33298  ellpi  33341  idlsrgval  33471  rprmval  33484  dimval  33591  dimvalfi  33592  smatfval  33769  lmatval  33787  ispcmp  33831  qqhval2  33958  rrhval  33972  xrhval  33994  esumc  34027  esumpad  34031  esumpcvgval  34054  ofcfval3  34078  issiga  34088  baselsiga  34091  sigasspw  34092  issgon  34099  isrnsigau  34103  sigagenval  34116  ispisys2  34129  cldssbrsiga  34163  sxval  34166  ismeas  34175  cnmbfm  34240  mbfmcnt  34245  elcarsg  34282  sitmval  34326  eulerpartlemt0  34346  sseqval  34365  sseqmw  34368  sseqp1  34372  orvcval  34435  orvcval4  34438  ballotlemsv  34487  prcinf  35083  satf  35333  satfv1lem  35342  satefv  35394  mrexval  35481  mrsubffval  35487  msubffval  35503  mclsval  35543  eldm3  35736  opelco3  35750  elima4  35751  elfix2  35880  elsingles  35894  fvimage  35907  funpartlem  35918  elaltxp  35951  brcolinear2  36034  ellines  36128  topfneec  36331  topfneec2  36332  fnejoin2  36345  limsucncmpi  36421  findabrcl  36430  weiunse  36444  bj-ififc  36558  elelb  36873  bj-pwvrelb  36874  bj-sngltag  36959  bj-xtagex  36965  bj-elsnb  37037  bj-epelg  37044  bj-evalval  37051  bj-ismoore  37081  bj-ideqg1  37140  bj-ideqg1ALT  37141  bj-elid6  37146  bj-diagval  37150  bj-eldiag2  37153  bj-isrvec  37270  finxpreclem1  37365  finxpreclem3  37369  elghomlem2OLD  37868  isrngo  37879  isdivrngo  37932  br1cnvres  38245  riotasv2d  38933  riotasv3d  38936  lshpset  38954  lsatset  38966  lcvfbr  38996  lflset  39035  lkrfval  39063  lkrval2  39066  islshpkrN  39096  ldualset  39101  cmtfvalN  39186  cvrfval  39244  pats  39261  llnset  39482  lplnset  39506  lvolset  39549  lineset  39715  pointsetN  39718  psubspset  39721  pmapfval  39733  paddfval  39774  pclfvalN  39866  polfvalN  39881  psubclsetN  39913  watfvalN  39969  lhpset  39972  lautset  40059  pautsetN  40075  ldilfset  40085  ltrnfset  40094  dilfsetN  40129  trnfsetN  40132  trlfset  40137  tgrpfset  40721  tendofset  40735  erngfset  40776  erngfset-rN  40784  dvafset  40981  diaffval  41007  dvhfset  41057  docaffvalN  41098  djaffvalN  41110  dibffval  41117  dicffval  41151  dihffval  41207  dochffval  41326  djhffval  41373  lpolsetN  41459  lcdfval  41565  mapdffval  41603  hvmapffval  41735  hdmap1ffval  41772  hdmapffval  41803  hgmapffval  41862  hlhilset  41911  elrfi  42683  nacsfix  42701  mapfzcons2  42708  sbc2rexgOLD  42777  sbc4rexgOLD  42779  setindtrs  43015  wepwso  43033  hbtlem1  43113  hbtlem7  43115  mendval  43169  oaltublim  43280  omord2lim  43290  cnvtrucl0  43614  eliunov2  43669  iunrelexpmin1  43698  iunrelexpmin2  43702  trclfvcom  43713  cnvtrclfv  43714  trclimalb2  43716  trclfvdecomr  43718  gneispacef2  44126  gneispacern2  44129  gneispace0nelrn  44130  addrval  44457  subrval  44458  mulvval  44459  elixpconstg  45066  mptfnd  45220  upbdrech  45289  climf  45609  climf2  45653  liminfval  45746  dvcosre  45899  itgsinexplem1  45941  itgsubsticclem  45962  dmvolss  45972  stoweidlem26  46013  stoweidlem35  46022  stirlinglem14  46074  fourierdlem42  46136  fourierdlem81  46174  fourierdlem89  46182  fourierdlem91  46184  salgenval  46308  elsprel  47435  sprval  47439  prprval  47474  isisubgr  47821  isgrim  47841  uhgrimisgrgric  47872  grtri  47880  isgrlim  47922  usgrexmpl2nb0  47963  usgrexmpl2nb1  47964  usgrexmpl2nb3  47966  upwlksfval  48024  isupwlkg  48026  intopval  48091  clintopval  48093  assintopval  48094  rngcvalALTV  48154  ringcvalALTV  48178  dmatbas  48293  lincop  48298  lcoop  48301  fdivval  48433  blenval  48465  itcoval  48555  itcoval1  48557  itcoval2  48558  itcoval3  48559  itcovalsucov  48562  lines  48625  spheres  48640  discsnterm  49266