Theorem elex 2812

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395  ∃wex 1538   ∈ wcel 2200  Vcvv 2800

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2802

This theorem is referenced by:  elexi  2813  elexd  2814  elisset  2815  vtoclgft  2852  vtoclgf  2860  vtoclg1f  2861  vtocl2gf  2864  vtocl3gf  2865  spcimgft  2880  spcimegft  2882  elab4g  2953  elrabf  2958  mob  2986  sbcex  3038  sbcel1v  3092  sbcabel  3112  csbcomg  3148  csbvarg  3153  csbiebt  3165  csbnestgf  3178  csbidmg  3182  sbcco3g  3183  csbco3g  3184  eldif  3207  ssv  3247  elun  3346  elin  3388  elif  3615  elpwb  3660  snidb  3697  snssg  3805  dfopg  3858  eluni  3894  eliun  3972  csbexga  4215  nvel  4220  class2seteq  4251  axpweq  4259  snelpwi  4301  opexg  4318  elopab  4350  epelg  4385  elon2  4471  unexg  4538  reuhypd  4566  sucexg  4594  onsucb  4599  onsucelsucr  4604  sucunielr  4606  en2lp  4650  peano2  4691  peano2b  4711  opelvvg  4773  opeliunxp  4779  opeliunxp2  4868  ideqg  4879  elrnmptg  4982  imasng  5099  iniseg  5106  opswapg  5221  elxp4  5222  elxp5  5223  dmmptg  5232  iota2  5314  fnmpt  5456  fvexg  5654  fvelimab  5698  mptfvex  5728  fvmptdf  5730  fvmptdv2  5732  mpteqb  5733  fvmptt  5734  fvmptf  5735  fvopab6  5739  fsn2  5817  fmptpr  5841  eloprabga  6103  ovmpos  6140  ov2gf  6141  ovmpodxf  6142  ovmpox  6145  ovmpoga  6146  ovmpodf  6148  ovi3  6154  ovelrn  6166  suppssfv  6226  suppssov1  6227  offval3  6291  1stexg  6325  2ndexg  6326  elxp6  6327  elxp7  6328  releldm2  6343  fnmpo  6362  mpofvex  6365  mpoexg  6371  opeliunxp2f  6399  brtpos2  6412  rdgtfr  6535  rdgruledefgg  6536  frec0g  6558  sucinc2  6609  nntri3or  6656  relelec  6739  ecdmn0m  6741  mapvalg  6822  pmvalg  6823  elpmg  6828  elixp2  6866  mptelixpg  6898  elixpsn  6899  map1  6982  rex2dom  6991  mapdom1g  7028  mapxpen  7029  fival  7160  elfi2  7162  djulclr  7239  djurclr  7240  djulcl  7241  djurcl  7242  djulclb  7245  inl11  7255  djuss  7260  1stinl  7264  2ndinl  7265  1stinr  7266  2ndinr  7267  ismkvnex  7345  omniwomnimkv  7357  isacnm  7408  cc4n  7480  elinp  7684  addnqprlemfl  7769  addnqprlemfu  7770  mulnqprlemfl  7785  mulnqprlemfu  7786  recexprlemell  7832  recexprlemelu  7833  wrdexg  11114  wrdsymb0  11136  lswwrd  11150  ccatfvalfi  11159  swrdval  11219  swrd00g  11220  pfxval  11245  cats1fvn  11335  cats1fvnd  11336  s2fv1g  11359  s2leng  11360  s2dmg  11361  shftfvalg  11369  clim  11832  climmpt  11851  climshft2  11857  4sqlem2  12952  isstruct2r  13083  slotex  13099  setsvalg  13102  setsfun0  13108  setscom  13112  ressvalsets  13137  ressbasid  13143  restval  13318  topnvalg  13324  tgval  13335  ptex  13337  prdsex  13342  pwsval  13364  pwsbas  13365  pwselbasb  13366  pwssnf1o  13371  imasex  13378  qusex  13398  qusaddvallemg  13406  xpsfrnel2  13419  plusffvalg  13435  grpidvalg  13446  gsum0g  13469  sgrp1  13484  issubmnd  13515  pws0g  13524  issubm  13545  grppropstrg  13592  grpinvfvalg  13615  grpinvfng  13617  grpsubfvalg  13618  grpressid  13634  mulgfvalg  13698  mulgex  13700  mulgfng  13701  issubg  13750  subgex  13753  releqgg  13797  eqgex  13798  eqgfval  13799  isghm  13820  ablressid  13912  mgpvalg  13926  mgptopng  13932  rngressid  13957  rngpropd  13958  ringidvalg  13964  dfur2g  13965  issrg  13968  iscrng2  14018  ringressid  14066  opprvalg  14072  dvdsrex  14102  unitgrp  14120  unitabl  14121  unitlinv  14130  unitrinv  14131  isnzr2  14188  issubrng  14203  issubrg  14225  subrgugrp  14244  aprap  14290  islmod  14295  scaffvalg  14310  lsssetm  14360  islssmg  14362  lspfval  14392  lspval  14394  lspcl  14395  lspex  14399  sraval  14441  rlmvalg  14458  rlmsubg  14462  rlmvnegg  14469  ixpsnbasval  14470  lidlvalg  14475  rspvalg  14476  lidlex  14477  rspex  14478  2idlvalg  14507  zrhvalg  14622  zlmval  14631  mplvalcoe  14694  mplbascoe  14695  mplplusgg  14707  toponsspwpwg  14736  eltg  14766  eltg2  14767  restbasg  14882  tgrest  14883  txvalex  14968  txval  14969  ispsmet  15037  ismet  15058  isxmet  15059  xmetunirn  15072  blfvalps  15099  vtxvalg  15857  iedgvalg  15858  vtxex  15859  edgvalg  15900  vtxdgfval  16094  wksfval  16119  iswlkg  16126  wlkvtxeledgg  16141  trlsfvalg  16178  clwwlkg  16188  clwwlkng  16200  eupthsg  16240  bj-vtoclgft  16307  djucllem  16332  bj-nvel  16428  2omapen  16531  pw1mapen  16533