Theorem elex 2825

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, 5-Aug-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 1666	. 2 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) → ∃𝑥 𝑥 = 𝐴)
2		df-clel 2228	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
3		isset 2820	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4	1, 2, 3	3imtr4i 201	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398  ∃wex 1541   ∈ wcel 2203  Vcvv 2813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-v 2815

This theorem is referenced by:  elexi  2826  elexd  2827  elisset  2828  vtoclgft  2865  vtoclgf  2873  vtoclg1f  2874  vtocl2gf  2877  vtocl3gf  2878  spcimgft  2893  spcimegft  2895  elab4g  2966  elrabf  2971  mob  2999  sbcex  3051  sbcel1v  3105  sbcabel  3125  csbcomg  3161  csbvarg  3166  csbiebt  3178  csbnestgf  3191  csbidmg  3195  sbcco3g  3196  csbco3g  3197  eldif  3220  ssv  3260  elun  3360  elin  3402  elif  3634  elpwb  3679  snidb  3719  eldifvsn  3826  snssg  3828  dfopg  3881  eluni  3917  eliun  3995  csbexga  4238  nvel  4243  class2seteq  4276  axpweq  4284  snelpwi  4327  opexg  4344  elopab  4376  epelg  4411  elon2  4497  unexg  4564  reuhypd  4592  sucexg  4620  onsucb  4625  onsucelsucr  4630  sucunielr  4632  en2lp  4676  peano2  4717  peano2b  4737  opelvvg  4799  opeliunxp  4805  opeliunxp2  4895  ideqg  4906  elrnmptg  5009  imasng  5127  iniseg  5134  opswapg  5249  elxp4  5250  elxp5  5251  dmmptg  5260  iota2  5342  fnmpt  5485  fvexg  5689  fvelimab  5733  mptfvex  5763  fvmptdf  5765  fvmptdv2  5767  mpteqb  5768  fvmptt  5769  fvmptf  5770  fvopab6  5774  fsn2  5851  fmptpr  5876  eloprabga  6140  ovmpos  6177  ov2gf  6178  ovmpodxf  6179  ovmpox  6182  ovmpoga  6183  ovmpodf  6185  ovi3  6191  ovelrn  6203  suppssov1  6263  offval3  6327  1stexg  6361  2ndexg  6362  elxp6  6363  elxp7  6364  releldm2  6379  fnmpo  6398  mpofvex  6401  mpoexg  6407  suppval  6437  opeliunxp2f  6469  brtpos2  6482  rdgtfr  6605  rdgruledefgg  6606  frec0g  6628  sucinc2  6679  nntri3or  6726  relelec  6809  ecdmn0m  6811  mapvalg  6892  pmvalg  6893  elpmg  6898  elixp2  6937  mptelixpg  6969  elixpsn  6970  map1  7054  rex2dom  7063  mapdom1g  7100  mapxpen  7101  fival  7257  elfi2  7259  2omapen  7270  djulclr  7340  djurclr  7341  djulcl  7342  djurcl  7343  djulclb  7346  inl11  7356  djuss  7361  1stinl  7365  2ndinl  7366  1stinr  7367  2ndinr  7368  ismkvnex  7446  omniwomnimkv  7458  isacnm  7510  cc4n  7585  elinp  7789  addnqprlemfl  7874  addnqprlemfu  7875  mulnqprlemfl  7890  mulnqprlemfu  7891  recexprlemell  7937  recexprlemelu  7938  hashmap  11192  wrdexg  11235  wrdsymb0  11257  lswwrd  11271  ccatfvalfi  11280  swrdval  11340  swrd00g  11341  pfxval  11366  cats1fvn  11456  cats1fvnd  11457  s2fv1g  11480  s2leng  11481  s2dmg  11482  shftfvalg  11503  clim  11966  climmpt  11985  climshft2  11991  4sqlem2  13087  isstruct2r  13223  slotex  13239  setsvalg  13242  setsfun0  13248  setscom  13252  ressvalsets  13277  ressbasid  13283  restval  13458  topnvalg  13464  tgval  13475  ptex  13477  prdsex  13482  pwsval  13504  pwsbas  13505  pwselbasb  13506  pwssnf1o  13511  imasex  13518  qusex  13538  qusaddvallemg  13546  xpsfrnel2  13559  plusffvalg  13575  grpidvalg  13586  gsum0g  13609  sgrp1  13624  issubmnd  13655  pws0g  13664  issubm  13685  grppropstrg  13732  grpinvfvalg  13755  grpinvfng  13757  grpsubfvalg  13758  grpressid  13774  mulgfvalg  13838  mulgex  13840  mulgfng  13841  issubg  13890  subgex  13893  releqgg  13937  eqgex  13938  eqgfval  13939  isghm  13960  ablressid  14052  mgpvalg  14067  mgptopng  14073  rngressid  14098  rngpropd  14099  ringidvalg  14105  dfur2g  14106  issrg  14109  iscrng2  14159  ringressid  14207  opprvalg  14213  dvdsrex  14243  unitgrp  14261  unitabl  14262  unitlinv  14271  unitrinv  14272  isnzr2  14329  issubrng  14344  issubrg  14366  subrgugrp  14385  aprap  14432  islmod  14439  scaffvalg  14454  lsssetm  14504  islssmg  14506  lspfval  14536  lspval  14538  lspcl  14539  lspex  14543  sraval  14585  rlmvalg  14602  rlmsubg  14606  rlmvnegg  14613  ixpsnbasval  14614  lidlvalg  14619  rspvalg  14620  lidlex  14621  rspex  14622  2idlvalg  14651  zrhvalg  14766  zlmval  14775  mplvalcoe  14845  mplbascoe  14846  mplplusgg  14858  toponsspwpwg  14887  eltg  14917  eltg2  14918  restbasg  15033  tgrest  15034  txvalex  15119  txval  15120  ispsmet  15188  ismet  15209  isxmet  15210  xmetunirn  15223  blfvalps  15250  vtxvalg  16011  iedgvalg  16012  vtxex  16013  edgvalg  16054  vtxdgfval  16283  wksfval  16317  iswlkg  16324  wlkvtxeledgg  16339  trlsfvalg  16378  clwwlkg  16388  clwwlkng  16400  eupthsg  16440  bj-vtoclgft  16547  djucllem  16572  bj-nvel  16667  pw1mapen  16770