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  3574  snidb  3611  dfopg  3761  eluni  3797  eliun  3875  csbexga  4115  nvel  4120  class2seteq  4147  axpweq  4155  snelpwi  4195  opexg  4211  elopab  4241  epelg  4273  elon2  4359  unexg  4426  reuhypd  4454  sucexg  4480  sucelon  4485  onsucelsucr  4490  sucunielr  4492  en2lp  4536  peano2  4577  peano2b  4597  opelvvg  4658  opeliunxp  4664  opeliunxp2  4749  ideqg  4760  elrnmptg  4861  imasng  4974  iniseg  4981  opswapg  5095  elxp4  5096  elxp5  5097  dmmptg  5106  iota2  5186  fnmpt  5322  fvexg  5513  fvelimab  5550  mptfvex  5579  fvmptdf  5581  fvmptdv2  5583  mpteqb  5584  fvmptt  5585  fvmptf  5586  fvopab6  5590  fsn2  5667  fmptpr  5685  eloprabga  5937  ovmpos  5973  ov2gf  5974  ovmpodxf  5975  ovmpox  5978  ovmpoga  5979  ovmpodf  5981  ovi3  5986  ovelrn  5998  suppssfv  6054  suppssov1  6055  offval3  6110  1stexg  6143  2ndexg  6144  elxp6  6145  elxp7  6146  releldm2  6161  fnmpo  6178  mpofvex  6179  mpoexg  6187  opeliunxp2f  6214  brtpos2  6227  rdgtfr  6350  rdgruledefgg  6351  frec0g  6373  sucinc2  6422  nntri3or  6469  relelec  6549  ecdmn0m  6551  mapvalg  6632  pmvalg  6633  elpmg  6638  elixp2  6676  mptelixpg  6708  elixpsn  6709  map1  6786  mapdom1g  6821  mapxpen  6822  fival  6943  elfi2  6945  djulclr  7022  djurclr  7023  djulcl  7024  djurcl  7025  djulclb  7028  inl11  7038  djuss  7043  1stinl  7047  2ndinl  7048  1stinr  7049  2ndinr  7050  ismkvnex  7127  omniwomnimkv  7139  cc4n  7220  elinp  7423  addnqprlemfl  7508  addnqprlemfu  7509  mulnqprlemfl  7524  mulnqprlemfu  7525  recexprlemell  7571  recexprlemelu  7572  shftfvalg  10769  clim  11231  climmpt  11250  climshft2  11256  4sqlem2  12328  isstruct2r  12414  slotex  12430  setsvalg  12433  setsfun0  12439  setscom  12443  restval  12572  topnvalg  12578  plusffvalg  12603  grpidvalg  12614  sgrp1  12638  issubm  12682  toponsspwpwg  12773  tgval  12802  eltg  12805  eltg2  12806  restbasg  12921  tgrest  12922  txvalex  13007  txval  13008  ispsmet  13076  ismet  13097  isxmet  13098  xmetunirn  13111  blfvalps  13138  bj-vtoclgft  13769  djucllem  13794  bj-nvel  13892