Theorem elex 3493

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.)

Assertion

Ref	Expression
elex	⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)

Proof of Theorem elex

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		exsimpl 1872	. 2 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) → ∃𝑥 𝑥 = 𝐴)
2		dfclel 2812	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
3		isset 3488	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4	1, 2, 3	3imtr4i 292	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542  ∃wex 1782   ∈ wcel 2107  Vcvv 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477

This theorem is referenced by:  elexi  3494  elexd  3495  prcnel  3498  vtoclgf  3555  vtocl2gf  3561  vtocl3gf  3562  vtocl2g  3563  vtocl3g  3564  spcimgft  3578  spcgv  3587  spc3egv  3594  elab4g  3674  elrabf  3680  elrab  3684  class2seteq  3701  mob  3714  sbcex  3788  sbcel1v  3849  sbcabel  3873  csbiebt  3924  eldif  3959  elin  3965  ssv  4007  elun  4149  csbnestgfw  4420  sbcco3gw  4423  csbnestgf  4425  sbcco3g  4428  csbco3g  4429  csbvarg  4432  sbccsb2  4435  elpwb  4611  pwidb  4624  elpr2g  4653  elpr2OLD  4655  snidb  4664  ifpr  4696  snssg  4788  eldifvsn  4801  preqsnd  4860  elpreqpr  4868  dfopg  4872  eluni  4912  eliun  5002  csbexg  5311  nvel  5317  axpweq  5349  reusv2lem4  5400  elopab  5528  epelg  5582  opelvvg  5718  opeliunxp2  5839  opelres  5988  imasng  6083  elimasni  6091  iniseg  6097  inisegn0  6098  dmmptg  6242  elon2  6376  ordsssuc2  6456  iota2  6533  fnmptf  6687  fnmpt  6691  fvelimab  6965  mpteqb  7018  fvmptt  7019  fvmptf  7020  fvopab5  7031  fvopab6  7032  fprg  7153  eloprabga  7516  eloprabgaOLD  7517  ovmpos  7556  ov2gf  7557  ovmpox  7561  ovmpoga  7562  ovmpt3rab1  7664  brrpssg  7715  sorpssi  7719  unexg  7736  elpwun  7756  ordeleqon  7769  onintrab  7784  sucexg  7793  sucexeloni  7797  ordsucelsuc  7810  onzsl  7835  dmfexALT  7901  elxp5  7914  offval3  7969  releldm2  8029  fnmpo  8055  mpoexg  8063  mptmpoopabbrdOLD  8069  bropfvvvv  8078  fsplitfpar  8104  suppval  8148  opeliunxp2f  8195  brtpos2  8217  undefval  8261  tfr2b  8396  tz7.49  8445  oeordi  8587  relelec  8748  ecdmn0  8750  mapvalg  8830  pmvalg  8831  elpmg  8837  elixp2  8895  mptelixpg  8929  elixpsn  8931  2pwuninel  9132  rex2dom  9246  fival  9407  elfi2  9409  dffi2  9418  elfiun  9425  wemapso2lem  9547  harval  9555  brwdom  9562  fowdom  9566  brwdom2  9568  brwdom3  9577  en2lp  9601  cantnfsuc  9665  rankvalb  9792  rankwflem  9810  rankr1g  9827  r1pwALT  9841  r1rankid  9854  djulcl  9905  djurcl  9906  inlresf  9909  inrresf  9911  djuss  9915  1stinl  9922  2ndinl  9923  1stinr  9924  2ndinr  9925  cardval3  9947  dfac8alem  10024  isacn  10039  numacn  10044  acndom  10046  cardinfima  10092  unialeph  10096  ackbij1lem5  10219  cflm  10245  isf32lem2  10349  isfin1-2  10380  itunifval  10411  numth3  10465  ttukeylem1  10504  cardidg  10543  ondomon  10558  elwina  10681  elina  10682  wuncval  10737  tskmval  10834  eltskm  10838  recmulnq  10959  elnp  10982  elnpi  10983  npomex  10991  elfzp12  13580  seqp1  13981  hashinf  14295  hashxnn0  14299  hashnn0pnf  14302  hashxrcl  14317  prsshashgt1  14370  hashmap  14395  lsw  14514  ccatfval  14523  ccats1alpha  14569  swrdval  14593  pfxval  14623  splval  14701  splcl  14702  revval  14710  reps  14720  s3sndisj  14914  s3iunsndisj  14915  trclfv  14947  relexp0g  14969  relexpsucnnr  14972  relexp1g  14973  limsupcl  15417  limsupval  15418  clim  15438  rlim  15439  hashbcval  16935  isstruct2  17082  setsvalg  17099  setsfun0  17105  setscom  17113  strfvnd  17118  setsid  17141  ressval  17176  ressinbas  17190  restval  17372  pwsval  17432  xpsfrnel2  17510  ismre  17534  oppcval  17657  oppccatf  17674  brssc  17761  rescval  17774  issubc  17785  isfunc  17814  homadm  17990  homacd  17991  uncfval  18187  pltfval  18284  lubfval  18303  glbfval  18316  joinfval  18326  meetfval  18340  p0val  18380  p1val  18381  oduclatb  18460  ipoval  18483  pws0g  18661  frmdval  18732  vrmdfval  18737  efmnd  18751  efmnd2hash  18775  eqgfval  19056  gaid  19163  cntzfval  19184  elsymgbas  19241  symg2hash  19259  pmtrfval  19318  symggen  19338  gexval  19446  lsmfval  19506  pj1fval  19562  frgpval  19626  vrgpfval  19634  dmdprd  19868  dprdw  19880  pws1  20138  pwsmgp  20140  dvdsr  20176  isrim0OLD  20259  lssset  20544  lspfval  20584  islbs  20687  sraval  20789  zlmval  21065  psgnevpmb  21140  ocvfval  21219  cssval  21235  thlval  21248  dsmmval  21289  dsmmbase  21290  frlmval  21303  uvcfval  21339  islinds  21364  ltbval  21598  evlsval  21649  coe1fval  21729  evls1fval  21838  matval  21911  oftpos  21954  dmatval  21994  scmatval  22006  smadiadetglem2  22174  cpmat  22211  mat2pmatfval  22225  cpm2mfval  22251  decpmatval0  22266  pm2mpval  22297  chpmatfval  22332  basdif0  22456  tgval  22458  eltg  22460  eltg2  22461  neipeltop  22633  ordtval  22693  islocfin  23021  txval  23068  qtopval  23199  isfbas  23333  isfildlem  23361  fmval  23447  fmf  23449  isfcls  23513  alexsubb  23550  tsmsfbas  23632  ustval  23707  elutop  23738  isusp  23766  ispsmet  23810  ismet  23829  isxmet  23830  blfvalps  23889  metustel  24059  tngval  24148  elpi1  24561  rrxval  24904  q1peqb  25672  ig1pval  25690  taylfval  25871  ulmval  25892  elno  27149  nosupno  27206  noetalem2  27245  oldlim  27381  negsval  27500  iscgrg  27763  isismt  27785  legval  27835  ishlg  27853  ishpg  28010  iscgra  28060  isinag  28089  isleag  28098  iseqlg  28118  ttgval  28126  ttgvalOLD  28127  xmstrkgc  28143  cplgr2vpr  28690  vtxdgfval  28724  ewlksfval  28858  wksfval  28866  iswlkg  28870  wwlksnon  29105  wspthsnon  29106  avril1  29716  ispligb  29730  gidval  29765  isvcOLD  29832  0vfval  29859  elunop  31125  rabexgfGS  31739  disjdifprg  31806  disjdifprg2  31807  abfmpunirn  31877  rabfmpunirn  31878  hashgt1  32020  mntoval  32152  tocycval  32267  evpmval  32304  altgnsg  32308  sgnsv  32319  inftmrel  32326  isinftm  32327  resvval  32441  idlsrgval  32617  rprmval  32633  dimval  32686  dimvalfi  32687  smatfval  32775  lmatval  32793  ispcmp  32837  qqhval2  32962  rrhval  32976  xrhval  32998  indv  33010  esumc  33049  esumpad  33053  esumpcvgval  33076  ofcfval3  33100  issiga  33110  baselsiga  33113  sigasspw  33114  issgon  33121  isrnsigau  33125  sigagenval  33138  ispisys2  33151  cldssbrsiga  33185  sxval  33188  ismeas  33197  cnmbfm  33262  mbfmcnt  33267  elcarsg  33304  sitmval  33348  eulerpartlemt0  33368  sseqval  33387  sseqmw  33390  sseqp1  33394  orvcval  33456  orvcval4  33459  ballotlemsv  33508  satf  34344  satfv1lem  34353  satefv  34405  mrexval  34492  mrsubffval  34498  msubffval  34514  mclsval  34554  eldm3  34731  opelco3  34746  elima4  34747  elfix2  34876  elsingles  34890  fvimage  34903  funpartlem  34914  elaltxp  34947  brcolinear2  35030  ellines  35124  topfneec  35240  topfneec2  35241  fnejoin2  35254  limsucncmpi  35330  findabrcl  35339  bj-ififc  35459  elelb  35777  bj-pwvrelb  35778  bj-sngltag  35864  bj-xtagex  35870  bj-elsnb  35942  bj-epelg  35949  bj-evalval  35956  bj-ismoore  35986  bj-ideqg1  36045  bj-ideqg1ALT  36046  bj-elid6  36051  bj-diagval  36055  bj-eldiag2  36058  bj-isrvec  36175  finxpreclem1  36270  finxpreclem3  36274  elghomlem2OLD  36754  isrngo  36765  isdivrngo  36818  br1cnvres  37137  riotasv2d  37827  riotasv3d  37830  lshpset  37848  lsatset  37860  lcvfbr  37890  lflset  37929  lkrfval  37957  lkrval2  37960  islshpkrN  37990  ldualset  37995  cmtfvalN  38080  cvrfval  38138  pats  38155  llnset  38376  lplnset  38400  lvolset  38443  lineset  38609  pointsetN  38612  psubspset  38615  pmapfval  38627  paddfval  38668  pclfvalN  38760  polfvalN  38775  psubclsetN  38807  watfvalN  38863  lhpset  38866  lautset  38953  pautsetN  38969  ldilfset  38979  ltrnfset  38988  dilfsetN  39023  trnfsetN  39026  trlfset  39031  tgrpfset  39615  tendofset  39629  erngfset  39670  erngfset-rN  39678  dvafset  39875  diaffval  39901  dvhfset  39951  docaffvalN  39992  djaffvalN  40004  dibffval  40011  dicffval  40045  dihffval  40101  dochffval  40220  djhffval  40267  lpolsetN  40353  lcdfval  40459  mapdffval  40497  hvmapffval  40629  hdmap1ffval  40666  hdmapffval  40697  hgmapffval  40756  hlhilset  40805  elrab2w  41410  elrfi  41432  nacsfix  41450  mapfzcons2  41457  sbc2rexgOLD  41526  sbc4rexgOLD  41528  setindtrs  41764  wepwso  41785  hbtlem1  41865  hbtlem7  41867  rgspnval  41910  mendval  41925  oaltublim  42040  omord2lim  42050  cnvtrucl0  42375  eliunov2  42430  iunrelexpmin1  42459  iunrelexpmin2  42463  trclfvcom  42474  cnvtrclfv  42475  trclimalb2  42477  trclfvdecomr  42479  gneispacef2  42887  gneispacern2  42890  gneispace0nelrn  42891  addrval  43225  subrval  43226  mulvval  43227  elixpconstg  43778  mptfnd  43945  upbdrech  44015  climf  44338  climf2  44382  liminfval  44475  dvcosre  44628  itgsinexplem1  44670  itgsubsticclem  44691  dmvolss  44701  stoweidlem26  44742  stoweidlem35  44751  stirlinglem14  44803  fourierdlem42  44865  fourierdlem81  44903  fourierdlem89  44911  fourierdlem91  44913  salgenval  45037  elsprel  46143  sprval  46147  prprval  46182  upwlksfval  46513  isupwlkg  46515  intopval  46612  clintopval  46614  assintopval  46615  isrngisom  46694  rngcvalALTV  46859  rnghmsscmap  46872  ringcvalALTV  46905  rhmsscmap  46918  dmatbas  47084  lincop  47089  lcoop  47092  fdivval  47225  blenval  47257  itcoval  47347  itcoval1  47349  itcoval2  47350  itcoval3  47351  itcovalsucov  47354  lines  47417  spheres  47432