Theorem elex 2697

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1331  ∃wex 1468   ∈ wcel 1480  Vcvv 2686

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-v 2688

This theorem is referenced by:  elexi  2698  elexd  2699  elisset  2700  vtoclgft  2736  vtoclgf  2744  vtoclg1f  2745  vtocl2gf  2748  vtocl3gf  2749  spcimgft  2762  spcimegft  2764  elab4g  2833  elrabf  2838  mob  2866  sbcex  2917  sbcel1v  2971  sbcabel  2990  csbcomg  3025  csbvarg  3030  csbiebt  3039  csbnestgf  3052  csbidmg  3056  sbcco3g  3057  csbco3g  3058  eldif  3080  ssv  3119  elun  3217  elin  3259  elpwb  3520  snidb  3555  dfopg  3703  eluni  3739  eliun  3817  csbexga  4056  nvel  4061  class2seteq  4087  axpweq  4095  snelpwi  4134  opexg  4150  elopab  4180  epelg  4212  elon2  4298  unexg  4364  reuhypd  4392  sucexg  4414  sucelon  4419  onsucelsucr  4424  sucunielr  4426  en2lp  4469  peano2  4509  peano2b  4528  opelvvg  4588  opeliunxp  4594  opeliunxp2  4679  ideqg  4690  elrnmptg  4791  imasng  4904  iniseg  4911  opswapg  5025  elxp4  5026  elxp5  5027  dmmptg  5036  iota2  5114  fnmpt  5249  fvexg  5440  fvelimab  5477  mptfvex  5506  fvmptdf  5508  fvmptdv2  5510  mpteqb  5511  fvmptt  5512  fvmptf  5513  fvopab6  5517  fsn2  5594  fmptpr  5612  eloprabga  5858  ovmpos  5894  ov2gf  5895  ovmpodxf  5896  ovmpox  5899  ovmpoga  5900  ovmpodf  5902  ovi3  5907  ovelrn  5919  suppssfv  5978  suppssov1  5979  offval3  6032  1stexg  6065  2ndexg  6066  elxp6  6067  elxp7  6068  releldm2  6083  fnmpo  6100  mpofvex  6101  mpoexg  6109  opeliunxp2f  6135  brtpos2  6148  rdgtfr  6271  rdgruledefgg  6272  frec0g  6294  sucinc2  6342  nntri3or  6389  relelec  6469  ecdmn0m  6471  mapvalg  6552  pmvalg  6553  elpmg  6558  elixp2  6596  mptelixpg  6628  elixpsn  6629  map1  6706  mapdom1g  6741  mapxpen  6742  fival  6858  elfi2  6860  djulclr  6934  djurclr  6935  djulcl  6936  djurcl  6937  djulclb  6940  inl11  6950  djuss  6955  1stinl  6959  2ndinl  6960  1stinr  6961  2ndinr  6962  ismkvnex  7029  elinp  7282  addnqprlemfl  7367  addnqprlemfu  7368  mulnqprlemfl  7383  mulnqprlemfu  7384  recexprlemell  7430  recexprlemelu  7431  shftfvalg  10590  clim  11050  climmpt  11069  climshft2  11075  isstruct2r  11970  slotex  11986  setsvalg  11989  setsfun0  11995  setscom  11999  restval  12126  topnvalg  12132  toponsspwpwg  12189  tgval  12218  eltg  12221  eltg2  12222  restbasg  12337  tgrest  12338  txvalex  12423  txval  12424  ispsmet  12492  ismet  12513  isxmet  12514  xmetunirn  12527  blfvalps  12554  bj-vtoclgft  12982  djucllem  13007  bj-nvel  13095