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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ∃wex 1811   ∈ wcel 2146  Vcvv 3454

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456

This theorem is used by:  elexi  3476  elexd  3477  prcnel  3479  vtoclgf  3533  vtocl2gf  3535  vtocl3gf  3536  vtocl2g  3537  vtocl3g  3538  spcgv  3554  spc3egv  3561  elab4g  3640  elrabf  3645  elrab  3648  elrab2w  3653  class2seteq  3665  mob  3678  sbcex  3752  sbcel1v  3807  sbcabel  3829  csbiebt  3880  ssv  3937  eldif  4052  elin  4096  elun  4155  csbnestgfw  4383  sbcco3gw  4386  csbnestgf  4388  sbcco3g  4391  csbco3g  4392  csbvarg  4395  sbccsb2  4398  elpwb  4568  pwidg  4581  pwidb  4583  elpr2g  4610  snidb  4622  ifpr  4654  snssg  4744  eldifvsn  4760  preqsnd  4817  elpreqpr  4825  dfopg  4841  eluni  4873  eliun  4958  csbexg  5267  nvelOLD  5280  axpweq  5316  reusv2lem4  5367  elopab  5505  epelg  5556  opelvvg  5696  opeliunxp2  5820  opelres  5981  imasng  6088  elimasni  6095  iniseg  6101  inisegn0  6102  dmmptg  6250  elon2  6380  ordsssuc2  6463  iota2  6535  fnmptf  6686  fnmpt  6690  fvelimab  6968  mpteqb  7024  fvmptt  7025  fvmptf  7026  fvopab5  7038  fvopab6  7039  fprg  7170  eloprabga  7539  ovmpos  7578  ov2gf  7579  ovmpox  7583  ovmpoga  7584  ovmpt3rab1  7689  brrpssg  7751  sorpssi  7755  elpwun  7793  ordeleqon  7806  onintrab  7820  sucexg  7829  sucexeloni  7833  ordsucelsuc  7843  onzsl  7867  dmfexALT  7930  elxp5  7945  fabexg  7960  f1oabexg  7963  offval3  8004  releldm2  8064  fnmpo  8091  mpoexg  8100  bropfvvvv  8114  fsplitfpar  8142  suppval  8192  opeliunxp2f  8241  brtpos2  8263  undefval  8308  tfr2b  8418  tz7.49  8469  oeordi  8610  relelec  8779  ecdmn0  8784  mapvalg  8870  pmvalg  8871  elpmg  8877  elixp2  8943  mptelixpg  8977  elixpsn  8979  2pwuninel  9165  ordfin  9245  rex2dom  9258  fival  9417  elfi2  9419  dffi2  9428  elfiun  9435  wemapso2lem  9559  harval  9567  brwdom  9574  fowdom  9578  brwdom2  9580  brwdom3  9589  en2lp  9620  cantnfsuc  9684  rankvalb  9818  rankwflem  9837  rankr1g  9857  r1pwALT  9873  r1rankid  9888  djulcl  10004  djurcl  10005  inlresf  10008  inrresf  10010  djuss  10014  1stinl  10021  2ndinl  10022  1stinr  10023  2ndinr  10024  cardval3  10046  dfac8alem  10121  isacn  10136  numacn  10141  acndom  10143  cardinfima  10189  unialeph  10193  ackbij1lem5  10314  cflm  10340  isf32lem2  10445  isfin1-2  10476  itunifval  10507  numth3  10561  ttukeylem1  10600  imadomnum  10627  cardidg  10645  ondomon  10660  elwina  10784  elina  10785  wuncval  10840  tskmval  10937  eltskm  10941  recmulnq  11062  elnp  11085  elnpi  11086  npomex  11094  indv  12335  elfzp12  13750  seqp1  14172  hashinf  14492  hashxnn0  14496  hashnn0pnf  14499  hashxrcl  14514  prsshashgt1  14568  hashmap  14593  lsw  14722  ccatfval  14731  ccats1alpha  14781  swrdval  14805  pfxval  14837  splval  14914  splcl  14915  revval  14923  reps  14935  s3sndisj  15135  s3iunsndisj  15136  trclfv  15168  relexp0g  15190  relexpsucnnr  15193  relexp1g  15194  limsupcl  15655  limsupval  15656  clim  15676  rlim  15677  hashbcval  17195  isstruct2  17342  setsvalg  17359  setsfun0  17365  setscom  17373  strfvnd  17378  setsid  17400  ressval  17426  ressinbas  17438  restval  17612  pwsval  17672  xpsfrnel2  17751  ismre  17775  oppcval  17902  oppccatf  17917  brssc  18004  rescval  18017  issubc  18025  isfunc  18054  homadm  18230  homacd  18231  uncfval  18423  pltfval  18518  lubfval  18537  glbfval  18550  joinfval  18560  meetfval  18574  p0val  18614  p1val  18615  oduclatb  18696  ipoval  18719  pws0g  18982  frmdval  19062  vrmdfval  19067  efmnd  19081  efmnd2hash  19105  eqgfval  19403  gaid  19528  cntzfval  19549  elsymgbas  19603  symg2hash  19621  pmtrfval  19679  symggen  19699  gexval  19807  lsmfval  19867  pj1fval  19923  frgpval  19987  vrgpfval  19995  dmdprd  20229  dprdw  20241  pws1  20569  pwsmgp  20571  dvdsr  20607  isrngim  20690  rgspnval  20879  rnghmsscmap  20897  rhmsscmap  20926  lssset  21223  lspfval  21263  islbs  21366  sraval  21465  zlmval  21836  psgnevpmb  21908  ocvfval  21987  cssval  22003  thlval  22016  dsmmval  22055  dsmmbase  22056  frlmval  22069  uvcfval  22105  islinds  22130  ltbval  22367  evlsval  22410  coe1fval  22538  evls1fval  22652  matval  22741  oftpos  22782  dmatval  22822  scmatval  22834  smadiadetglem2  23002  cpmat  23042  mat2pmatfval  23056  cpm2mfval  23082  decpmatval0  23097  pm2mpval  23128  chpmatfval  23163  basdif0  23286  tgval  23288  eltg  23290  eltg2  23291  neipeltop  23462  ordtval  23522  islocfin  23851  txval  23898  qtopval  24029  isfbas  24163  isfildlem  24191  fmval  24277  fmf  24279  isfcls  24343  alexsubb  24380  tsmsfbas  24462  ustval  24537  elutop  24567  isusp  24595  ispsmet  24638  ismet  24657  isxmet  24658  blfvalps  24717  metustel  24884  tngval  24973  elpi1  25381  rrxval  25723  q1peqb  26489  ig1pval  26509  taylfval  26701  ulmval  26722  elno  28018  nosupno  28075  noetalem2  28114  nulslts  28176  oldlim  28288  negsval  28426  elz12s  28873  iscgrg  28990  isismt  29012  legval  29062  ishlg2  29080  ishlg  29083  ishpg  29252  iscgra  29331  isinag  29372  isleag  29381  angmgmval  29409  iseqlg  29427  ttgval  29467  xmstrkgc  29478  cplgr2vpr  30029  vtxdgfval  30063  ewlksfval  30197  wksfval  30205  iswlkg  30209  wwlksnon  30455  wspthsnon  30456  avril1  31079  ispligb  31094  gidval  31129  isvcOLD  31196  0vfval  31223  elunop  32489  rabexgfGS  33152  disjdifprg  33226  disjdifprg2  33227  abfmpunirn  33303  rabfmpunirn  33304  hashgt1  33456  mntoval  33599  tocycval  33725  evpmval  33762  altgnsg  33766  sgnsv  33777  inftmrel  33797  isinftm  33798  resvval  33946  ellpi  33984  idlsrgval  34091  rprmval  34104  dimval  34289  dimvalfi  34290  smatfval  34483  lmatval  34501  ispcmp  34545  qqhval2  34670  rrhval  34684  xrhval  34706  esumc  34739  esumpad  34743  esumpcvgval  34766  ofcfval3  34790  issiga  34800  baselsiga  34803  sigasspw  34804  issgon  34811  isrnsigau  34815  sigagenval  34829  ispisys2  34842  cldssbrsiga  34876  sxval  34879  ismeas  34888  cnmbfm  34951  mbfmcnt  34956  elcarsg  34993  sitmval  35037  eulerpartlemt0  35057  sseqval  35076  sseqmw  35079  sseqp1  35083  orvcval  35146  orvcval4  35149  ballotlemsv  35198  acnum  35829  prcinf  35855  satf  36242  satfv1lem  36251  satefv  36303  mrexval  36390  mrsubffval  36396  msubffval  36412  mclsval  36452  eldm3  36656  opelco3  36669  elima4  36670  elfix2  36796  elsingles  36810  fvimage  36823  funpartlem  36836  elaltxp  36870  brcolinear2  36953  ellines  37047  topfneec  37273  topfneec2  37274  fnejoin2  37287  limsucncmpi  37363  findabrcl  37372  weiunse  37386  ttcwf2  37443  bj-ififc  37582  elelb  37939  bj-pwvrelb  37940  bj-sngltag  38026  bj-xtagex  38032  bj-elsnb  38118  bj-epelg  38125  bj-evalval  38138  bj-ismoore  38168  bj-ideqg1  38228  bj-ideqg1ALT  38229  bj-elid6  38234  bj-diagval  38238  bj-eldiag2  38241  bj-isrvec  38358  finxpreclem1  38455  finxpreclem3  38459  elghomlem2OLD  38963  isrngo  38974  isdivrngo  39027  br1cnvres  39349  riotasv2d  40157  riotasv3d  40160  lshpset  40178  lsatset  40190  lcvfbr  40220  lflset  40259  lkrfval  40287  lkrval2  40290  islshpkrN  40320  ldualset  40325  cmtfvalN  40410  cvrfval  40468  pats  40485  llnset  40705  lplnset  40729  lvolset  40772  lineset  40938  pointsetN  40941  psubspset  40944  pmapfval  40956  paddfval  40997  pclfvalN  41089  polfvalN  41104  psubclsetN  41136  watfvalN  41192  lhpset  41195  lautset  41282  pautsetN  41298  ldilfset  41308  ltrnfset  41317  dilfsetN  41352  trnfsetN  41355  trlfset  41360  tgrpfset  41944  tendofset  41958  erngfset  41999  erngfset-rN  42007  dvafset  42204  diaffval  42230  dvhfset  42280  docaffvalN  42321  djaffvalN  42333  dibffval  42340  dicffval  42374  dihffval  42430  dochffval  42549  djhffval  42596  lpolsetN  42682  lcdfval  42788  mapdffval  42826  hvmapffval  42958  hdmap1ffval  42995  hdmapffval  43026  hgmapffval  43085  hlhilset  43134  elrfi  43848  nacsfix  43866  mapfzcons2  43873  setindtrs  44175  wepwso  44193  hbtlem1  44268  hbtlem7  44270  mendval  44324  oaltublim  44435  omord2lim  44445  cnvtrucl0  44767  eliunov2  44822  iunrelexpmin1  44851  iunrelexpmin2  44855  trclfvcom  44866  cnvtrclfv  44867  trclimalb2  44869  trclfvdecomr  44871  gneispacef2  45279  gneispacern2  45282  gneispace0nelrn  45283  addrval  45590  subrval  45591  mulvval  45592  orbitclmpt  46090  elixpconstg  46246  mptfnd  46396  upbdrech  46463  climf  46776  climf2  46818  liminfval  46911  dvcosre  47064  itgsinexplem1  47106  itgsubsticclem  47127  dmvolss  47137  stoweidlem26  47178  stoweidlem35  47187  stirlinglem14  47239  fourierdlem42  47301  fourierdlem81  47339  fourierdlem89  47347  fourierdlem91  47349  salgenval  47473  elsprel  48699  sprval  48703  prprval  48738  isisubgr  49102  isgrim  49122  uhgrimisgrgric  49171  grtri  49180  isgrlim  49222  usgrexmpl2nb0  49271  usgrexmpl2nb1  49272  usgrexmpl2nb3  49274  upwlksfval  49375  isupwlkg  49377  intopval  49441  clintopval  49443  assintopval  49444  rngcvalALTV  49504  ringcvalALTV  49528  dmatbas  49657  lincop  49662  lcoop  49665  fdivval  49793  blenval  49825  itcoval  49915  itcoval1  49917  itcoval2  49918  itcoval3  49919  itcovalsucov  49922  lines  49986  spheres  50000  discsnterm  50854  termolmd  50995