Theorem elex 2788

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1373  ∃wex 1516   ∈ wcel 2178  Vcvv 2776

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-v 2778

This theorem is referenced by:  elexi  2789  elexd  2790  elisset  2791  vtoclgft  2828  vtoclgf  2836  vtoclg1f  2837  vtocl2gf  2840  vtocl3gf  2841  spcimgft  2856  spcimegft  2858  elab4g  2929  elrabf  2934  mob  2962  sbcex  3014  sbcel1v  3068  sbcabel  3088  csbcomg  3124  csbvarg  3129  csbiebt  3141  csbnestgf  3154  csbidmg  3158  sbcco3g  3159  csbco3g  3160  eldif  3183  ssv  3223  elun  3322  elin  3364  elif  3591  elpwb  3636  snidb  3673  snssg  3778  dfopg  3831  eluni  3867  eliun  3945  csbexga  4188  nvel  4193  class2seteq  4223  axpweq  4231  snelpwi  4273  opexg  4290  elopab  4322  epelg  4355  elon2  4441  unexg  4508  reuhypd  4536  sucexg  4564  onsucb  4569  onsucelsucr  4574  sucunielr  4576  en2lp  4620  peano2  4661  peano2b  4681  opelvvg  4742  opeliunxp  4748  opeliunxp2  4836  ideqg  4847  elrnmptg  4949  imasng  5066  iniseg  5073  opswapg  5188  elxp4  5189  elxp5  5190  dmmptg  5199  iota2  5280  fnmpt  5422  fvexg  5618  fvelimab  5658  mptfvex  5688  fvmptdf  5690  fvmptdv2  5692  mpteqb  5693  fvmptt  5694  fvmptf  5695  fvopab6  5699  fsn2  5777  fmptpr  5799  eloprabga  6055  ovmpos  6092  ov2gf  6093  ovmpodxf  6094  ovmpox  6097  ovmpoga  6098  ovmpodf  6100  ovi3  6106  ovelrn  6118  suppssfv  6177  suppssov1  6178  offval3  6242  1stexg  6276  2ndexg  6277  elxp6  6278  elxp7  6279  releldm2  6294  fnmpo  6311  mpofvex  6314  mpoexg  6320  opeliunxp2f  6347  brtpos2  6360  rdgtfr  6483  rdgruledefgg  6484  frec0g  6506  sucinc2  6555  nntri3or  6602  relelec  6685  ecdmn0m  6687  mapvalg  6768  pmvalg  6769  elpmg  6774  elixp2  6812  mptelixpg  6844  elixpsn  6845  map1  6928  rex2dom  6934  mapdom1g  6969  mapxpen  6970  fival  7098  elfi2  7100  djulclr  7177  djurclr  7178  djulcl  7179  djurcl  7180  djulclb  7183  inl11  7193  djuss  7198  1stinl  7202  2ndinl  7203  1stinr  7204  2ndinr  7205  ismkvnex  7283  omniwomnimkv  7295  isacnm  7346  cc4n  7418  elinp  7622  addnqprlemfl  7707  addnqprlemfu  7708  mulnqprlemfl  7723  mulnqprlemfu  7724  recexprlemell  7770  recexprlemelu  7771  wrdexg  11042  wrdsymb0  11063  lswwrd  11077  ccatfvalfi  11086  swrdval  11139  swrd00g  11140  pfxval  11165  shftfvalg  11244  clim  11707  climmpt  11726  climshft2  11732  4sqlem2  12827  isstruct2r  12958  slotex  12974  setsvalg  12977  setsfun0  12983  setscom  12987  ressvalsets  13011  ressbasid  13017  restval  13192  topnvalg  13198  tgval  13209  ptex  13211  prdsex  13216  pwsval  13238  pwsbas  13239  pwselbasb  13240  pwssnf1o  13245  imasex  13252  qusex  13272  qusaddvallemg  13280  xpsfrnel2  13293  plusffvalg  13309  grpidvalg  13320  gsum0g  13343  sgrp1  13358  issubmnd  13389  pws0g  13398  issubm  13419  grppropstrg  13466  grpinvfvalg  13489  grpinvfng  13491  grpsubfvalg  13492  grpressid  13508  mulgfvalg  13572  mulgex  13574  mulgfng  13575  issubg  13624  subgex  13627  releqgg  13671  eqgex  13672  eqgfval  13673  isghm  13694  ablressid  13786  mgpvalg  13800  mgptopng  13806  rngressid  13831  rngpropd  13832  ringidvalg  13838  dfur2g  13839  issrg  13842  iscrng2  13892  ringressid  13940  opprvalg  13946  reldvdsrsrg  13969  dvdsrex  13975  unitgrp  13993  unitabl  13994  unitlinv  14003  unitrinv  14004  isnzr2  14061  issubrng  14076  issubrg  14098  subrgugrp  14117  aprap  14163  islmod  14168  scaffvalg  14183  lsssetm  14233  islssmg  14235  lspfval  14265  lspval  14267  lspcl  14268  lspex  14272  sraval  14314  rlmvalg  14331  rlmsubg  14335  rlmvnegg  14342  ixpsnbasval  14343  lidlvalg  14348  rspvalg  14349  lidlex  14350  rspex  14351  2idlvalg  14380  zrhvalg  14495  zlmval  14504  mplvalcoe  14567  mplbascoe  14568  mplplusgg  14580  toponsspwpwg  14609  eltg  14639  eltg2  14640  restbasg  14755  tgrest  14756  txvalex  14841  txval  14842  ispsmet  14910  ismet  14931  isxmet  14932  xmetunirn  14945  blfvalps  14972  vtxvalg  15730  iedgvalg  15731  vtxex  15732  edgvalg  15771  bj-vtoclgft  15911  djucllem  15936  bj-nvel  16032  2omapen  16133  pw1mapen  16135