Theorem elex 2771

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 1628	. 2 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) → ∃𝑥 𝑥 = 𝐴)
2		df-clel 2189	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
3		isset 2766	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4	1, 2, 3	3imtr4i 201	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364  ∃wex 1503   ∈ wcel 2164  Vcvv 2760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-v 2762

This theorem is referenced by:  elexi  2772  elexd  2773  elisset  2774  vtoclgft  2811  vtoclgf  2819  vtoclg1f  2820  vtocl2gf  2823  vtocl3gf  2824  spcimgft  2837  spcimegft  2839  elab4g  2910  elrabf  2915  mob  2943  sbcex  2995  sbcel1v  3049  sbcabel  3068  csbcomg  3104  csbvarg  3109  csbiebt  3121  csbnestgf  3134  csbidmg  3138  sbcco3g  3139  csbco3g  3140  eldif  3163  ssv  3202  elun  3301  elin  3343  elpwb  3612  snidb  3649  snssg  3753  dfopg  3803  eluni  3839  eliun  3917  csbexga  4158  nvel  4163  class2seteq  4193  axpweq  4201  snelpwi  4242  opexg  4258  elopab  4289  epelg  4322  elon2  4408  unexg  4475  reuhypd  4503  sucexg  4531  onsucb  4536  onsucelsucr  4541  sucunielr  4543  en2lp  4587  peano2  4628  peano2b  4648  opelvvg  4709  opeliunxp  4715  opeliunxp2  4803  ideqg  4814  elrnmptg  4915  imasng  5031  iniseg  5038  opswapg  5153  elxp4  5154  elxp5  5155  dmmptg  5164  iota2  5245  fnmpt  5381  fvexg  5574  fvelimab  5614  mptfvex  5644  fvmptdf  5646  fvmptdv2  5648  mpteqb  5649  fvmptt  5650  fvmptf  5651  fvopab6  5655  fsn2  5733  fmptpr  5751  eloprabga  6006  ovmpos  6043  ov2gf  6044  ovmpodxf  6045  ovmpox  6048  ovmpoga  6049  ovmpodf  6051  ovi3  6057  ovelrn  6069  suppssfv  6128  suppssov1  6129  offval3  6188  1stexg  6222  2ndexg  6223  elxp6  6224  elxp7  6225  releldm2  6240  fnmpo  6257  mpofvex  6260  mpoexg  6266  opeliunxp2f  6293  brtpos2  6306  rdgtfr  6429  rdgruledefgg  6430  frec0g  6452  sucinc2  6501  nntri3or  6548  relelec  6631  ecdmn0m  6633  mapvalg  6714  pmvalg  6715  elpmg  6720  elixp2  6758  mptelixpg  6790  elixpsn  6791  map1  6868  mapdom1g  6905  mapxpen  6906  fival  7031  elfi2  7033  djulclr  7110  djurclr  7111  djulcl  7112  djurcl  7113  djulclb  7116  inl11  7126  djuss  7131  1stinl  7135  2ndinl  7136  1stinr  7137  2ndinr  7138  ismkvnex  7216  omniwomnimkv  7228  cc4n  7333  elinp  7536  addnqprlemfl  7621  addnqprlemfu  7622  mulnqprlemfl  7637  mulnqprlemfu  7638  recexprlemell  7684  recexprlemelu  7685  wrdexg  10928  wrdsymb0  10949  shftfvalg  10965  clim  11427  climmpt  11446  climshft2  11452  4sqlem2  12530  isstruct2r  12632  slotex  12648  setsvalg  12651  setsfun0  12657  setscom  12661  ressvalsets  12685  ressbasid  12691  restval  12859  topnvalg  12865  tgval  12876  ptex  12878  prdsex  12883  imasex  12891  qusex  12911  qusaddvallemg  12919  xpsfrnel2  12932  plusffvalg  12948  grpidvalg  12959  gsum0g  12982  sgrp1  12997  issubmnd  13026  issubm  13047  grppropstrg  13094  grpinvfvalg  13117  grpinvfng  13119  grpsubfvalg  13120  grpressid  13136  mulgfvalg  13194  mulgex  13196  mulgfng  13197  issubg  13246  subgex  13249  releqgg  13293  eqgex  13294  eqgfval  13295  isghm  13316  ablressid  13408  mgpvalg  13422  mgptopng  13428  rngressid  13453  rngpropd  13454  ringidvalg  13460  dfur2g  13461  issrg  13464  iscrng2  13514  ringressid  13562  opprvalg  13568  reldvdsrsrg  13591  dvdsrex  13597  unitgrp  13615  unitabl  13616  unitlinv  13625  unitrinv  13626  isnzr2  13683  issubrng  13698  issubrg  13720  subrgugrp  13739  aprap  13785  islmod  13790  scaffvalg  13805  lsssetm  13855  islssmg  13857  lspfval  13887  lspval  13889  lspcl  13890  lspex  13894  sraval  13936  rlmvalg  13953  rlmsubg  13957  rlmvnegg  13964  ixpsnbasval  13965  lidlvalg  13970  rspvalg  13971  lidlex  13972  rspex  13973  2idlvalg  14002  zrhvalg  14117  zlmval  14126  toponsspwpwg  14201  eltg  14231  eltg2  14232  restbasg  14347  tgrest  14348  txvalex  14433  txval  14434  ispsmet  14502  ismet  14523  isxmet  14524  xmetunirn  14537  blfvalps  14564  bj-vtoclgft  15337  djucllem  15362  bj-nvel  15459