Theorem elex 2827

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398  ∃wex 1541   ∈ wcel 2205  Vcvv 2815

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-v 2817

This theorem is referenced by:  elexi  2828  elexd  2829  elisset  2830  vtoclgft  2867  vtoclgf  2875  vtoclg1f  2876  vtocl2gf  2879  vtocl3gf  2880  spcimgft  2895  spcimegft  2897  elab4g  2969  elrabf  2974  mob  3002  sbcex  3054  sbcel1v  3108  sbcabel  3128  csbcomg  3164  csbvarg  3169  csbiebt  3181  csbnestgf  3194  csbidmg  3198  sbcco3g  3199  csbco3g  3200  eldif  3223  ssv  3264  elun  3364  elin  3406  elif  3638  elpwb  3684  snidb  3724  eldifvsn  3831  snssg  3833  dfopg  3886  eluni  3922  eliun  4000  csbexga  4243  nvel  4248  class2seteq  4281  axpweq  4289  snelpwi  4332  opexg  4349  elopab  4381  epelg  4416  elon2  4502  unexg  4569  reuhypd  4597  sucexg  4625  onsucb  4630  onsucelsucr  4635  sucunielr  4637  en2lp  4681  peano2  4722  peano2b  4742  opelvvg  4804  opeliunxp  4810  opeliunxp2  4900  ideqg  4911  elrnmptg  5014  imasng  5132  iniseg  5139  opswapg  5254  elxp4  5255  elxp5  5256  dmmptg  5265  iota2  5347  fnmpt  5490  fvexg  5694  fvelimab  5738  mptfvex  5768  fvmptdf  5770  fvmptdv2  5772  mpteqb  5773  fvmptt  5774  fvmptf  5775  fvopab6  5779  fsn2  5856  fmptpr  5881  eloprabga  6148  ovmpos  6185  ov2gf  6186  ovmpodxf  6187  ovmpox  6190  ovmpoga  6191  ovmpodf  6193  ovi3  6199  ovelrn  6211  suppssov1  6272  offval3  6340  1stexg  6374  2ndexg  6375  elxp6  6376  elxp7  6377  releldm2  6392  fnmpo  6411  mpofvex  6414  mpoexg  6420  suppval  6450  opeliunxp2f  6482  brtpos2  6495  rdgtfr  6618  rdgruledefgg  6619  frec0g  6641  sucinc2  6692  nntri3or  6739  relelec  6822  ecdmn0m  6824  mapvalg  6905  pmvalg  6906  elpmg  6911  elixp2  6950  mptelixpg  6982  elixpsn  6983  map1  7067  rex2dom  7076  mapdom1g  7113  mapxpen  7114  fival  7270  elfi2  7272  2omapen  7283  djulclr  7353  djurclr  7354  djulcl  7355  djurcl  7356  djulclb  7359  inl11  7369  djuss  7374  1stinl  7378  2ndinl  7379  1stinr  7380  2ndinr  7381  ismkvnex  7459  omniwomnimkv  7471  isacnm  7523  cc4n  7601  elinp  7805  addnqprlemfl  7890  addnqprlemfu  7891  mulnqprlemfl  7906  mulnqprlemfu  7907  recexprlemell  7953  recexprlemelu  7954  hashmap  11217  wrdexg  11260  wrdsymb0  11282  lswwrd  11296  ccatfvalfi  11305  swrdval  11365  swrd00g  11366  pfxval  11391  cats1fvn  11481  cats1fvnd  11482  s2fv1g  11505  s2leng  11506  s2dmg  11507  shftfvalg  11528  clim  11991  climmpt  12010  climshft2  12016  4sqlem2  13112  ballotfilemsv  13197  isstruct2r  13307  slotex  13323  setsvalg  13326  setsfun0  13332  setscom  13336  ressvalsets  13361  ressbasid  13367  restval  13542  topnvalg  13548  tgval  13559  ptex  13561  imasex  13569  qusex  13589  qusaddvallemg  13597  xpsfrnel2  13610  plusffvalg  13625  grpidvalg  13636  gsum0g  13659  sgrp1  13674  issubmnd  13703  issubm  13727  grppropstrg  13774  grpinvfvalg  13797  grpinvfng  13799  grpsubfvalg  13800  grpressid  13816  mulgfvalg  13874  mulgex  13876  mulgfng  13877  issubg  13926  subgex  13929  releqgg  13973  eqgex  13974  eqgfval  13975  isghm  13996  ablressid  14088  prdsex  14114  pwsval  14146  pwsbas  14147  pwselbasb  14148  pwssnf1o  14153  pws0g  14155  mgpvalg  14162  mgptopng  14168  rngressid  14193  rngpropd  14194  ringidvalg  14204  dfur2g  14205  issrg  14208  iscrng2  14258  ringressid  14306  opprvalg  14312  opprringb  14324  dvdsrex  14343  unitgrp  14361  unitabl  14362  unitlinv  14371  unitrinv  14372  isnzr2  14429  issubrng  14445  issubrg  14467  subrgugrp  14486  aprap  14536  aprprop  14539  islmod  14565  scaffvalg  14580  lsssetm  14630  islssmg  14632  lspfval  14662  lspval  14664  lspcl  14665  lspex  14669  sraval  14711  rlmvalg  14728  rlmsubg  14732  rlmvnegg  14739  ixpsnbasval  14740  lidlvalg  14745  rspvalg  14746  lidlex  14747  rspex  14748  2idlvalg  14777  zrhvalg  14892  zlmval  14901  mplvalcoe  14971  mplbascoe  14972  mplplusgg  14984  toponsspwpwg  15013  eltg  15043  eltg2  15044  restbasg  15159  tgrest  15160  txvalex  15245  txval  15246  ispsmet  15314  ismet  15335  isxmet  15336  xmetunirn  15349  blfvalps  15376  vtxvalg  16137  iedgvalg  16138  vtxex  16139  edgvalg  16180  vtxdgfval  16409  wksfval  16443  iswlkg  16450  wlkvtxeledgg  16465  trlsfvalg  16504  clwwlkg  16514  clwwlkng  16526  eupthsg  16566  bj-vtoclgft  16673  djucllem  16698  bj-nvel  16793  pw1mapen  16896