Theorem elex 3509

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

Syntax hints:   → wi 4   = wceq 1537  ∃wex 1777   ∈ wcel 2108  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490

This theorem is referenced by:  elexi  3511  elexd  3512  prcnel  3515  spcimgfi1OLD  3560  vtoclgf  3581  vtocl2gf  3584  vtocl3gf  3585  vtocl2g  3586  vtocl3g  3587  spcgv  3609  spc3egv  3616  elab4g  3699  elrabf  3704  elrab  3708  elrab2w  3712  class2seteq  3726  mob  3739  sbcex  3814  sbcel1v  3875  sbcabel  3900  csbiebt  3951  eldif  3986  elin  3992  ssv  4033  elun  4176  csbnestgfw  4445  sbcco3gw  4448  csbnestgf  4450  sbcco3g  4453  csbco3g  4454  csbvarg  4457  sbccsb2  4460  elpwb  4630  pwidb  4643  elpr2g  4673  snidb  4683  ifpr  4716  snssg  4808  eldifvsn  4822  preqsnd  4883  elpreqpr  4891  dfopg  4895  eluni  4934  eliun  5019  csbexg  5328  nvel  5334  axpweq  5369  reusv2lem4  5419  elopab  5546  epelg  5600  opelvvg  5741  opeliunxp2  5863  opelres  6015  imasng  6113  elimasni  6121  iniseg  6127  inisegn0  6128  dmmptg  6273  elon2  6406  ordsssuc2  6486  iota2  6562  fnmptf  6716  fnmpt  6720  fvelimab  6994  mpteqb  7048  fvmptt  7049  fvmptf  7050  fvopab5  7062  fvopab6  7063  fprg  7189  eloprabga  7558  eloprabgaOLD  7559  ovmpos  7598  ov2gf  7599  ovmpox  7603  ovmpoga  7604  ovmpt3rab1  7708  brrpssg  7760  sorpssi  7764  unexgOLD  7784  elpwun  7804  ordeleqon  7817  onintrab  7832  sucexg  7841  sucexeloni  7845  ordsucelsuc  7858  onzsl  7883  dmfexALT  7948  elxp5  7963  fabexg  7976  f1oabexg  7980  offval3  8023  releldm2  8084  fnmpo  8110  mpoexg  8117  mptmpoopabbrdOLDOLD  8124  bropfvvvv  8133  fsplitfpar  8159  suppval  8203  opeliunxp2f  8251  brtpos2  8273  undefval  8317  tfr2b  8452  tz7.49  8501  oeordi  8643  relelec  8810  ecdmn0  8812  mapvalg  8894  pmvalg  8895  elpmg  8901  elixp2  8959  mptelixpg  8993  elixpsn  8995  2pwuninel  9198  rex2dom  9309  fival  9481  elfi2  9483  dffi2  9492  elfiun  9499  wemapso2lem  9621  harval  9629  brwdom  9636  fowdom  9640  brwdom2  9642  brwdom3  9651  en2lp  9675  cantnfsuc  9739  rankvalb  9866  rankwflem  9884  rankr1g  9901  r1pwALT  9915  r1rankid  9928  djulcl  9979  djurcl  9980  inlresf  9983  inrresf  9985  djuss  9989  1stinl  9996  2ndinl  9997  1stinr  9998  2ndinr  9999  cardval3  10021  dfac8alem  10098  isacn  10113  numacn  10118  acndom  10120  cardinfima  10166  unialeph  10170  ackbij1lem5  10292  cflm  10319  isf32lem2  10423  isfin1-2  10454  itunifval  10485  numth3  10539  ttukeylem1  10578  cardidg  10617  ondomon  10632  elwina  10755  elina  10756  wuncval  10811  tskmval  10908  eltskm  10912  recmulnq  11033  elnp  11056  elnpi  11057  npomex  11065  elfzp12  13663  seqp1  14067  hashinf  14384  hashxnn0  14388  hashnn0pnf  14391  hashxrcl  14406  prsshashgt1  14459  hashmap  14484  lsw  14612  ccatfval  14621  ccats1alpha  14667  swrdval  14691  pfxval  14721  splval  14799  splcl  14800  revval  14808  reps  14818  s3sndisj  15016  s3iunsndisj  15017  trclfv  15049  relexp0g  15071  relexpsucnnr  15074  relexp1g  15075  limsupcl  15519  limsupval  15520  clim  15540  rlim  15541  hashbcval  17049  isstruct2  17196  setsvalg  17213  setsfun0  17219  setscom  17227  strfvnd  17232  setsid  17255  ressval  17290  ressinbas  17304  restval  17486  pwsval  17546  xpsfrnel2  17624  ismre  17648  oppcval  17771  oppccatf  17788  brssc  17875  rescval  17888  issubc  17899  isfunc  17928  homadm  18107  homacd  18108  uncfval  18304  pltfval  18401  lubfval  18420  glbfval  18433  joinfval  18443  meetfval  18457  p0val  18497  p1val  18498  oduclatb  18577  ipoval  18600  pws0g  18808  frmdval  18886  vrmdfval  18891  efmnd  18905  efmnd2hash  18929  eqgfval  19216  gaid  19339  cntzfval  19360  elsymgbas  19415  symg2hash  19433  pmtrfval  19492  symggen  19512  gexval  19620  lsmfval  19680  pj1fval  19736  frgpval  19800  vrgpfval  19808  dmdprd  20042  dprdw  20054  pws1  20348  pwsmgp  20350  dvdsr  20388  isrngim  20471  isrim0OLD  20507  rnghmsscmap  20652  rhmsscmap  20681  lssset  20954  lspfval  20994  islbs  21098  sraval  21197  zlmval  21549  psgnevpmb  21628  ocvfval  21707  cssval  21723  thlval  21736  dsmmval  21777  dsmmbase  21778  frlmval  21791  uvcfval  21827  islinds  21852  ltbval  22084  evlsval  22133  coe1fval  22228  evls1fval  22344  matval  22436  oftpos  22479  dmatval  22519  scmatval  22531  smadiadetglem2  22699  cpmat  22736  mat2pmatfval  22750  cpm2mfval  22776  decpmatval0  22791  pm2mpval  22822  chpmatfval  22857  basdif0  22981  tgval  22983  eltg  22985  eltg2  22986  neipeltop  23158  ordtval  23218  islocfin  23546  txval  23593  qtopval  23724  isfbas  23858  isfildlem  23886  fmval  23972  fmf  23974  isfcls  24038  alexsubb  24075  tsmsfbas  24157  ustval  24232  elutop  24263  isusp  24291  ispsmet  24335  ismet  24354  isxmet  24355  blfvalps  24414  metustel  24584  tngval  24673  elpi1  25097  rrxval  25440  q1peqb  26215  ig1pval  26235  taylfval  26418  ulmval  26441  elno  27708  elnoOLD  27709  nosupno  27766  noetalem2  27805  oldlim  27943  negsval  28075  elzs12  28439  iscgrg  28538  isismt  28560  legval  28610  ishlg  28628  ishpg  28785  iscgra  28835  isinag  28864  isleag  28873  iseqlg  28893  ttgval  28901  ttgvalOLD  28902  xmstrkgc  28918  cplgr2vpr  29468  vtxdgfval  29503  ewlksfval  29637  wksfval  29645  iswlkg  29649  wwlksnon  29884  wspthsnon  29885  avril1  30495  ispligb  30509  gidval  30544  isvcOLD  30611  0vfval  30638  elunop  31904  rabexgfGS  32527  disjdifprg  32597  disjdifprg2  32598  abfmpunirn  32670  rabfmpunirn  32671  hashgt1  32815  mntoval  32955  tocycval  33101  evpmval  33138  altgnsg  33142  sgnsv  33153  inftmrel  33160  isinftm  33161  resvval  33318  ellpi  33366  idlsrgval  33496  rprmval  33509  dimval  33613  dimvalfi  33614  smatfval  33741  lmatval  33759  ispcmp  33803  qqhval2  33928  rrhval  33942  xrhval  33964  indv  33976  esumc  34015  esumpad  34019  esumpcvgval  34042  ofcfval3  34066  issiga  34076  baselsiga  34079  sigasspw  34080  issgon  34087  isrnsigau  34091  sigagenval  34104  ispisys2  34117  cldssbrsiga  34151  sxval  34154  ismeas  34163  cnmbfm  34228  mbfmcnt  34233  elcarsg  34270  sitmval  34314  eulerpartlemt0  34334  sseqval  34353  sseqmw  34356  sseqp1  34360  orvcval  34422  orvcval4  34425  ballotlemsv  34474  prcinf  35070  satf  35321  satfv1lem  35330  satefv  35382  mrexval  35469  mrsubffval  35475  msubffval  35491  mclsval  35531  eldm3  35723  opelco3  35738  elima4  35739  elfix2  35868  elsingles  35882  fvimage  35895  funpartlem  35906  elaltxp  35939  brcolinear2  36022  ellines  36116  topfneec  36321  topfneec2  36322  fnejoin2  36335  limsucncmpi  36411  findabrcl  36420  weiunse  36434  bj-ififc  36548  elelb  36863  bj-pwvrelb  36864  bj-sngltag  36949  bj-xtagex  36955  bj-elsnb  37027  bj-epelg  37034  bj-evalval  37041  bj-ismoore  37071  bj-ideqg1  37130  bj-ideqg1ALT  37131  bj-elid6  37136  bj-diagval  37140  bj-eldiag2  37143  bj-isrvec  37260  finxpreclem1  37355  finxpreclem3  37359  elghomlem2OLD  37846  isrngo  37857  isdivrngo  37910  br1cnvres  38225  riotasv2d  38913  riotasv3d  38916  lshpset  38934  lsatset  38946  lcvfbr  38976  lflset  39015  lkrfval  39043  lkrval2  39046  islshpkrN  39076  ldualset  39081  cmtfvalN  39166  cvrfval  39224  pats  39241  llnset  39462  lplnset  39486  lvolset  39529  lineset  39695  pointsetN  39698  psubspset  39701  pmapfval  39713  paddfval  39754  pclfvalN  39846  polfvalN  39861  psubclsetN  39893  watfvalN  39949  lhpset  39952  lautset  40039  pautsetN  40055  ldilfset  40065  ltrnfset  40074  dilfsetN  40109  trnfsetN  40112  trlfset  40117  tgrpfset  40701  tendofset  40715  erngfset  40756  erngfset-rN  40764  dvafset  40961  diaffval  40987  dvhfset  41037  docaffvalN  41078  djaffvalN  41090  dibffval  41097  dicffval  41131  dihffval  41187  dochffval  41306  djhffval  41353  lpolsetN  41439  lcdfval  41545  mapdffval  41583  hvmapffval  41715  hdmap1ffval  41752  hdmapffval  41783  hgmapffval  41842  hlhilset  41891  elrfi  42650  nacsfix  42668  mapfzcons2  42675  sbc2rexgOLD  42744  sbc4rexgOLD  42746  setindtrs  42982  wepwso  43000  hbtlem1  43080  hbtlem7  43082  rgspnval  43125  mendval  43140  oaltublim  43252  omord2lim  43262  cnvtrucl0  43586  eliunov2  43641  iunrelexpmin1  43670  iunrelexpmin2  43674  trclfvcom  43685  cnvtrclfv  43686  trclimalb2  43688  trclfvdecomr  43690  gneispacef2  44098  gneispacern2  44101  gneispace0nelrn  44102  addrval  44435  subrval  44436  mulvval  44437  elixpconstg  44991  mptfnd  45150  upbdrech  45220  climf  45543  climf2  45587  liminfval  45680  dvcosre  45833  itgsinexplem1  45875  itgsubsticclem  45896  dmvolss  45906  stoweidlem26  45947  stoweidlem35  45956  stirlinglem14  46008  fourierdlem42  46070  fourierdlem81  46108  fourierdlem89  46116  fourierdlem91  46118  salgenval  46242  elsprel  47349  sprval  47353  prprval  47388  isisubgr  47734  isgrim  47752  uhgrimisgrgric  47783  grtri  47791  isgrlim  47806  usgrexmpl2nb0  47846  usgrexmpl2nb1  47847  usgrexmpl2nb3  47849  upwlksfval  47858  isupwlkg  47860  intopval  47925  clintopval  47927  assintopval  47928  rngcvalALTV  47988  ringcvalALTV  48012  dmatbas  48132  lincop  48137  lcoop  48140  fdivval  48273  blenval  48305  itcoval  48395  itcoval1  48397  itcoval2  48398  itcoval3  48399  itcovalsucov  48402  lines  48465  spheres  48480