Theorem elex 2700

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1332  ∃wex 1469   ∈ wcel 1481  Vcvv 2689

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-v 2691

This theorem is referenced by:  elexi  2701  elexd  2702  elisset  2703  vtoclgft  2739  vtoclgf  2747  vtoclg1f  2748  vtocl2gf  2751  vtocl3gf  2752  spcimgft  2765  spcimegft  2767  elab4g  2837  elrabf  2842  mob  2870  sbcex  2921  sbcel1v  2975  sbcabel  2994  csbcomg  3030  csbvarg  3035  csbiebt  3044  csbnestgf  3057  csbidmg  3061  sbcco3g  3062  csbco3g  3063  eldif  3085  ssv  3124  elun  3222  elin  3264  elpwb  3525  snidb  3562  dfopg  3711  eluni  3747  eliun  3825  csbexga  4064  nvel  4069  class2seteq  4095  axpweq  4103  snelpwi  4142  opexg  4158  elopab  4188  epelg  4220  elon2  4306  unexg  4372  reuhypd  4400  sucexg  4422  sucelon  4427  onsucelsucr  4432  sucunielr  4434  en2lp  4477  peano2  4517  peano2b  4536  opelvvg  4596  opeliunxp  4602  opeliunxp2  4687  ideqg  4698  elrnmptg  4799  imasng  4912  iniseg  4919  opswapg  5033  elxp4  5034  elxp5  5035  dmmptg  5044  iota2  5122  fnmpt  5257  fvexg  5448  fvelimab  5485  mptfvex  5514  fvmptdf  5516  fvmptdv2  5518  mpteqb  5519  fvmptt  5520  fvmptf  5521  fvopab6  5525  fsn2  5602  fmptpr  5620  eloprabga  5866  ovmpos  5902  ov2gf  5903  ovmpodxf  5904  ovmpox  5907  ovmpoga  5908  ovmpodf  5910  ovi3  5915  ovelrn  5927  suppssfv  5986  suppssov1  5987  offval3  6040  1stexg  6073  2ndexg  6074  elxp6  6075  elxp7  6076  releldm2  6091  fnmpo  6108  mpofvex  6109  mpoexg  6117  opeliunxp2f  6143  brtpos2  6156  rdgtfr  6279  rdgruledefgg  6280  frec0g  6302  sucinc2  6350  nntri3or  6397  relelec  6477  ecdmn0m  6479  mapvalg  6560  pmvalg  6561  elpmg  6566  elixp2  6604  mptelixpg  6636  elixpsn  6637  map1  6714  mapdom1g  6749  mapxpen  6750  fival  6866  elfi2  6868  djulclr  6942  djurclr  6943  djulcl  6944  djurcl  6945  djulclb  6948  inl11  6958  djuss  6963  1stinl  6967  2ndinl  6968  1stinr  6969  2ndinr  6970  ismkvnex  7037  omniwomnimkv  7049  cc4n  7103  elinp  7306  addnqprlemfl  7391  addnqprlemfu  7392  mulnqprlemfl  7407  mulnqprlemfu  7408  recexprlemell  7454  recexprlemelu  7455  shftfvalg  10622  clim  11082  climmpt  11101  climshft2  11107  isstruct2r  12009  slotex  12025  setsvalg  12028  setsfun0  12034  setscom  12038  restval  12165  topnvalg  12171  toponsspwpwg  12228  tgval  12257  eltg  12260  eltg2  12261  restbasg  12376  tgrest  12377  txvalex  12462  txval  12463  ispsmet  12531  ismet  12552  isxmet  12553  xmetunirn  12566  blfvalps  12593  bj-vtoclgft  13153  djucllem  13178  bj-nvel  13266