Theorem elex 2814

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397  ∃wex 1540   ∈ wcel 2202  Vcvv 2802

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2804

This theorem is referenced by:  elexi  2815  elexd  2816  elisset  2817  vtoclgft  2854  vtoclgf  2862  vtoclg1f  2863  vtocl2gf  2866  vtocl3gf  2867  spcimgft  2882  spcimegft  2884  elab4g  2955  elrabf  2960  mob  2988  sbcex  3040  sbcel1v  3094  sbcabel  3114  csbcomg  3150  csbvarg  3155  csbiebt  3167  csbnestgf  3180  csbidmg  3184  sbcco3g  3185  csbco3g  3186  eldif  3209  ssv  3249  elun  3348  elin  3390  elif  3617  elpwb  3662  snidb  3699  snssg  3807  dfopg  3860  eluni  3896  eliun  3974  csbexga  4217  nvel  4222  class2seteq  4253  axpweq  4261  snelpwi  4303  opexg  4320  elopab  4352  epelg  4387  elon2  4473  unexg  4540  reuhypd  4568  sucexg  4596  onsucb  4601  onsucelsucr  4606  sucunielr  4608  en2lp  4652  peano2  4693  peano2b  4713  opelvvg  4775  opeliunxp  4781  opeliunxp2  4870  ideqg  4881  elrnmptg  4984  imasng  5101  iniseg  5108  opswapg  5223  elxp4  5224  elxp5  5225  dmmptg  5234  iota2  5316  fnmpt  5459  fvexg  5658  fvelimab  5702  mptfvex  5732  fvmptdf  5734  fvmptdv2  5736  mpteqb  5737  fvmptt  5738  fvmptf  5739  fvopab6  5743  fsn2  5821  fmptpr  5845  eloprabga  6107  ovmpos  6144  ov2gf  6145  ovmpodxf  6146  ovmpox  6149  ovmpoga  6150  ovmpodf  6152  ovi3  6158  ovelrn  6170  suppssfv  6230  suppssov1  6231  offval3  6295  1stexg  6329  2ndexg  6330  elxp6  6331  elxp7  6332  releldm2  6347  fnmpo  6366  mpofvex  6369  mpoexg  6375  opeliunxp2f  6403  brtpos2  6416  rdgtfr  6539  rdgruledefgg  6540  frec0g  6562  sucinc2  6613  nntri3or  6660  relelec  6743  ecdmn0m  6745  mapvalg  6826  pmvalg  6827  elpmg  6832  elixp2  6870  mptelixpg  6902  elixpsn  6903  map1  6986  rex2dom  6995  mapdom1g  7032  mapxpen  7033  fival  7168  elfi2  7170  djulclr  7247  djurclr  7248  djulcl  7249  djurcl  7250  djulclb  7253  inl11  7263  djuss  7268  1stinl  7272  2ndinl  7273  1stinr  7274  2ndinr  7275  ismkvnex  7353  omniwomnimkv  7365  isacnm  7417  cc4n  7489  elinp  7693  addnqprlemfl  7778  addnqprlemfu  7779  mulnqprlemfl  7794  mulnqprlemfu  7795  recexprlemell  7841  recexprlemelu  7842  wrdexg  11123  wrdsymb0  11145  lswwrd  11159  ccatfvalfi  11168  swrdval  11228  swrd00g  11229  pfxval  11254  cats1fvn  11344  cats1fvnd  11345  s2fv1g  11368  s2leng  11369  s2dmg  11370  shftfvalg  11378  clim  11841  climmpt  11860  climshft2  11866  4sqlem2  12961  isstruct2r  13092  slotex  13108  setsvalg  13111  setsfun0  13117  setscom  13121  ressvalsets  13146  ressbasid  13152  restval  13327  topnvalg  13333  tgval  13344  ptex  13346  prdsex  13351  pwsval  13373  pwsbas  13374  pwselbasb  13375  pwssnf1o  13380  imasex  13387  qusex  13407  qusaddvallemg  13415  xpsfrnel2  13428  plusffvalg  13444  grpidvalg  13455  gsum0g  13478  sgrp1  13493  issubmnd  13524  pws0g  13533  issubm  13554  grppropstrg  13601  grpinvfvalg  13624  grpinvfng  13626  grpsubfvalg  13627  grpressid  13643  mulgfvalg  13707  mulgex  13709  mulgfng  13710  issubg  13759  subgex  13762  releqgg  13806  eqgex  13807  eqgfval  13808  isghm  13829  ablressid  13921  mgpvalg  13935  mgptopng  13941  rngressid  13966  rngpropd  13967  ringidvalg  13973  dfur2g  13974  issrg  13977  iscrng2  14027  ringressid  14075  opprvalg  14081  dvdsrex  14111  unitgrp  14129  unitabl  14130  unitlinv  14139  unitrinv  14140  isnzr2  14197  issubrng  14212  issubrg  14234  subrgugrp  14253  aprap  14299  islmod  14304  scaffvalg  14319  lsssetm  14369  islssmg  14371  lspfval  14401  lspval  14403  lspcl  14404  lspex  14408  sraval  14450  rlmvalg  14467  rlmsubg  14471  rlmvnegg  14478  ixpsnbasval  14479  lidlvalg  14484  rspvalg  14485  lidlex  14486  rspex  14487  2idlvalg  14516  zrhvalg  14631  zlmval  14640  mplvalcoe  14703  mplbascoe  14704  mplplusgg  14716  toponsspwpwg  14745  eltg  14775  eltg2  14776  restbasg  14891  tgrest  14892  txvalex  14977  txval  14978  ispsmet  15046  ismet  15067  isxmet  15068  xmetunirn  15081  blfvalps  15108  vtxvalg  15866  iedgvalg  15867  vtxex  15868  edgvalg  15909  vtxdgfval  16138  wksfval  16172  iswlkg  16179  wlkvtxeledgg  16194  trlsfvalg  16233  clwwlkg  16243  clwwlkng  16255  eupthsg  16295  bj-vtoclgft  16371  djucllem  16396  bj-nvel  16492  2omapen  16595  pw1mapen  16597