Theorem elex 2741

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 1610	. 2 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) → ∃𝑥 𝑥 = 𝐴)
2		df-clel 2166	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
3		isset 2736	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4	1, 2, 3	3imtr4i 200	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1348  ∃wex 1485   ∈ wcel 2141  Vcvv 2730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-v 2732

This theorem is referenced by:  elexi  2742  elexd  2743  elisset  2744  vtoclgft  2780  vtoclgf  2788  vtoclg1f  2789  vtocl2gf  2792  vtocl3gf  2793  spcimgft  2806  spcimegft  2808  elab4g  2879  elrabf  2884  mob  2912  sbcex  2963  sbcel1v  3017  sbcabel  3036  csbcomg  3072  csbvarg  3077  csbiebt  3088  csbnestgf  3101  csbidmg  3105  sbcco3g  3106  csbco3g  3107  eldif  3130  ssv  3169  elun  3268  elin  3310  elpwb  3576  snidb  3613  dfopg  3763  eluni  3799  eliun  3877  csbexga  4117  nvel  4122  class2seteq  4149  axpweq  4157  snelpwi  4197  opexg  4213  elopab  4243  epelg  4275  elon2  4361  unexg  4428  reuhypd  4456  sucexg  4482  sucelon  4487  onsucelsucr  4492  sucunielr  4494  en2lp  4538  peano2  4579  peano2b  4599  opelvvg  4660  opeliunxp  4666  opeliunxp2  4751  ideqg  4762  elrnmptg  4863  imasng  4976  iniseg  4983  opswapg  5097  elxp4  5098  elxp5  5099  dmmptg  5108  iota2  5188  fnmpt  5324  fvexg  5515  fvelimab  5552  mptfvex  5581  fvmptdf  5583  fvmptdv2  5585  mpteqb  5586  fvmptt  5587  fvmptf  5588  fvopab6  5592  fsn2  5670  fmptpr  5688  eloprabga  5940  ovmpos  5976  ov2gf  5977  ovmpodxf  5978  ovmpox  5981  ovmpoga  5982  ovmpodf  5984  ovi3  5989  ovelrn  6001  suppssfv  6057  suppssov1  6058  offval3  6113  1stexg  6146  2ndexg  6147  elxp6  6148  elxp7  6149  releldm2  6164  fnmpo  6181  mpofvex  6182  mpoexg  6190  opeliunxp2f  6217  brtpos2  6230  rdgtfr  6353  rdgruledefgg  6354  frec0g  6376  sucinc2  6425  nntri3or  6472  relelec  6553  ecdmn0m  6555  mapvalg  6636  pmvalg  6637  elpmg  6642  elixp2  6680  mptelixpg  6712  elixpsn  6713  map1  6790  mapdom1g  6825  mapxpen  6826  fival  6947  elfi2  6949  djulclr  7026  djurclr  7027  djulcl  7028  djurcl  7029  djulclb  7032  inl11  7042  djuss  7047  1stinl  7051  2ndinl  7052  1stinr  7053  2ndinr  7054  ismkvnex  7131  omniwomnimkv  7143  cc4n  7233  elinp  7436  addnqprlemfl  7521  addnqprlemfu  7522  mulnqprlemfl  7537  mulnqprlemfu  7538  recexprlemell  7584  recexprlemelu  7585  shftfvalg  10782  clim  11244  climmpt  11263  climshft2  11269  4sqlem2  12341  isstruct2r  12427  slotex  12443  setsvalg  12446  setsfun0  12452  setscom  12456  restval  12585  topnvalg  12591  plusffvalg  12616  grpidvalg  12627  sgrp1  12651  issubm  12695  grpinvfvalg  12745  grpinvfng  12747  grpsubfvalg  12748  toponsspwpwg  12814  tgval  12843  eltg  12846  eltg2  12847  restbasg  12962  tgrest  12963  txvalex  13048  txval  13049  ispsmet  13117  ismet  13138  isxmet  13139  xmetunirn  13152  blfvalps  13179  bj-vtoclgft  13810  djucllem  13835  bj-nvel  13932