Theorem elex 2737

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1343  ∃wex 1480   ∈ wcel 2136  Vcvv 2726

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-v 2728

This theorem is referenced by:  elexi  2738  elexd  2739  elisset  2740  vtoclgft  2776  vtoclgf  2784  vtoclg1f  2785  vtocl2gf  2788  vtocl3gf  2789  spcimgft  2802  spcimegft  2804  elab4g  2875  elrabf  2880  mob  2908  sbcex  2959  sbcel1v  3013  sbcabel  3032  csbcomg  3068  csbvarg  3073  csbiebt  3084  csbnestgf  3097  csbidmg  3101  sbcco3g  3102  csbco3g  3103  eldif  3125  ssv  3164  elun  3263  elin  3305  elpwb  3569  snidb  3606  dfopg  3756  eluni  3792  eliun  3870  csbexga  4110  nvel  4115  class2seteq  4142  axpweq  4150  snelpwi  4190  opexg  4206  elopab  4236  epelg  4268  elon2  4354  unexg  4421  reuhypd  4449  sucexg  4475  sucelon  4480  onsucelsucr  4485  sucunielr  4487  en2lp  4531  peano2  4572  peano2b  4592  opelvvg  4653  opeliunxp  4659  opeliunxp2  4744  ideqg  4755  elrnmptg  4856  imasng  4969  iniseg  4976  opswapg  5090  elxp4  5091  elxp5  5092  dmmptg  5101  iota2  5179  fnmpt  5314  fvexg  5505  fvelimab  5542  mptfvex  5571  fvmptdf  5573  fvmptdv2  5575  mpteqb  5576  fvmptt  5577  fvmptf  5578  fvopab6  5582  fsn2  5659  fmptpr  5677  eloprabga  5929  ovmpos  5965  ov2gf  5966  ovmpodxf  5967  ovmpox  5970  ovmpoga  5971  ovmpodf  5973  ovi3  5978  ovelrn  5990  suppssfv  6046  suppssov1  6047  offval3  6102  1stexg  6135  2ndexg  6136  elxp6  6137  elxp7  6138  releldm2  6153  fnmpo  6170  mpofvex  6171  mpoexg  6179  opeliunxp2f  6206  brtpos2  6219  rdgtfr  6342  rdgruledefgg  6343  frec0g  6365  sucinc2  6414  nntri3or  6461  relelec  6541  ecdmn0m  6543  mapvalg  6624  pmvalg  6625  elpmg  6630  elixp2  6668  mptelixpg  6700  elixpsn  6701  map1  6778  mapdom1g  6813  mapxpen  6814  fival  6935  elfi2  6937  djulclr  7014  djurclr  7015  djulcl  7016  djurcl  7017  djulclb  7020  inl11  7030  djuss  7035  1stinl  7039  2ndinl  7040  1stinr  7041  2ndinr  7042  ismkvnex  7119  omniwomnimkv  7131  cc4n  7212  elinp  7415  addnqprlemfl  7500  addnqprlemfu  7501  mulnqprlemfl  7516  mulnqprlemfu  7517  recexprlemell  7563  recexprlemelu  7564  shftfvalg  10760  clim  11222  climmpt  11241  climshft2  11247  4sqlem2  12319  isstruct2r  12405  slotex  12421  setsvalg  12424  setsfun0  12430  setscom  12434  restval  12562  topnvalg  12568  plusffvalg  12593  grpidvalg  12604  toponsspwpwg  12660  tgval  12689  eltg  12692  eltg2  12693  restbasg  12808  tgrest  12809  txvalex  12894  txval  12895  ispsmet  12963  ismet  12984  isxmet  12985  xmetunirn  12998  blfvalps  13025  bj-vtoclgft  13656  djucllem  13681  bj-nvel  13779