Theorem elex 2814

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397  ∃wex 1540   ∈ wcel 2202  Vcvv 2802

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2804

This theorem is referenced by:  elexi  2815  elexd  2816  elisset  2817  vtoclgft  2854  vtoclgf  2862  vtoclg1f  2863  vtocl2gf  2866  vtocl3gf  2867  spcimgft  2882  spcimegft  2884  elab4g  2955  elrabf  2960  mob  2988  sbcex  3040  sbcel1v  3094  sbcabel  3114  csbcomg  3150  csbvarg  3155  csbiebt  3167  csbnestgf  3180  csbidmg  3184  sbcco3g  3185  csbco3g  3186  eldif  3209  ssv  3249  elun  3348  elin  3390  elif  3617  elpwb  3662  snidb  3699  snssg  3807  dfopg  3860  eluni  3896  eliun  3974  csbexga  4217  nvel  4222  class2seteq  4253  axpweq  4261  snelpwi  4303  opexg  4320  elopab  4352  epelg  4387  elon2  4473  unexg  4540  reuhypd  4568  sucexg  4596  onsucb  4601  onsucelsucr  4606  sucunielr  4608  en2lp  4652  peano2  4693  peano2b  4713  opelvvg  4775  opeliunxp  4781  opeliunxp2  4870  ideqg  4881  elrnmptg  4984  imasng  5101  iniseg  5108  opswapg  5223  elxp4  5224  elxp5  5225  dmmptg  5234  iota2  5316  fnmpt  5459  fvexg  5658  fvelimab  5702  mptfvex  5732  fvmptdf  5734  fvmptdv2  5736  mpteqb  5737  fvmptt  5738  fvmptf  5739  fvopab6  5743  fsn2  5821  fmptpr  5846  eloprabga  6108  ovmpos  6145  ov2gf  6146  ovmpodxf  6147  ovmpox  6150  ovmpoga  6151  ovmpodf  6153  ovi3  6159  ovelrn  6171  suppssfv  6231  suppssov1  6232  offval3  6296  1stexg  6330  2ndexg  6331  elxp6  6332  elxp7  6333  releldm2  6348  fnmpo  6367  mpofvex  6370  mpoexg  6376  opeliunxp2f  6404  brtpos2  6417  rdgtfr  6540  rdgruledefgg  6541  frec0g  6563  sucinc2  6614  nntri3or  6661  relelec  6744  ecdmn0m  6746  mapvalg  6827  pmvalg  6828  elpmg  6833  elixp2  6871  mptelixpg  6903  elixpsn  6904  map1  6987  rex2dom  6996  mapdom1g  7033  mapxpen  7034  fival  7169  elfi2  7171  djulclr  7248  djurclr  7249  djulcl  7250  djurcl  7251  djulclb  7254  inl11  7264  djuss  7269  1stinl  7273  2ndinl  7274  1stinr  7275  2ndinr  7276  ismkvnex  7354  omniwomnimkv  7366  isacnm  7418  cc4n  7490  elinp  7694  addnqprlemfl  7779  addnqprlemfu  7780  mulnqprlemfl  7795  mulnqprlemfu  7796  recexprlemell  7842  recexprlemelu  7843  wrdexg  11124  wrdsymb0  11146  lswwrd  11160  ccatfvalfi  11169  swrdval  11229  swrd00g  11230  pfxval  11255  cats1fvn  11345  cats1fvnd  11346  s2fv1g  11369  s2leng  11370  s2dmg  11371  shftfvalg  11379  clim  11842  climmpt  11861  climshft2  11867  4sqlem2  12963  isstruct2r  13094  slotex  13110  setsvalg  13113  setsfun0  13119  setscom  13123  ressvalsets  13148  ressbasid  13154  restval  13329  topnvalg  13335  tgval  13346  ptex  13348  prdsex  13353  pwsval  13375  pwsbas  13376  pwselbasb  13377  pwssnf1o  13382  imasex  13389  qusex  13409  qusaddvallemg  13417  xpsfrnel2  13430  plusffvalg  13446  grpidvalg  13457  gsum0g  13480  sgrp1  13495  issubmnd  13526  pws0g  13535  issubm  13556  grppropstrg  13603  grpinvfvalg  13626  grpinvfng  13628  grpsubfvalg  13629  grpressid  13645  mulgfvalg  13709  mulgex  13711  mulgfng  13712  issubg  13761  subgex  13764  releqgg  13808  eqgex  13809  eqgfval  13810  isghm  13831  ablressid  13923  mgpvalg  13938  mgptopng  13944  rngressid  13969  rngpropd  13970  ringidvalg  13976  dfur2g  13977  issrg  13980  iscrng2  14030  ringressid  14078  opprvalg  14084  dvdsrex  14114  unitgrp  14132  unitabl  14133  unitlinv  14142  unitrinv  14143  isnzr2  14200  issubrng  14215  issubrg  14237  subrgugrp  14256  aprap  14302  islmod  14307  scaffvalg  14322  lsssetm  14372  islssmg  14374  lspfval  14404  lspval  14406  lspcl  14407  lspex  14411  sraval  14453  rlmvalg  14470  rlmsubg  14474  rlmvnegg  14481  ixpsnbasval  14482  lidlvalg  14487  rspvalg  14488  lidlex  14489  rspex  14490  2idlvalg  14519  zrhvalg  14634  zlmval  14643  mplvalcoe  14706  mplbascoe  14707  mplplusgg  14719  toponsspwpwg  14748  eltg  14778  eltg2  14779  restbasg  14894  tgrest  14895  txvalex  14980  txval  14981  ispsmet  15049  ismet  15070  isxmet  15071  xmetunirn  15084  blfvalps  15111  vtxvalg  15869  iedgvalg  15870  vtxex  15871  edgvalg  15912  vtxdgfval  16141  wksfval  16175  iswlkg  16182  wlkvtxeledgg  16197  trlsfvalg  16236  clwwlkg  16246  clwwlkng  16258  eupthsg  16298  bj-vtoclgft  16374  djucllem  16399  bj-nvel  16495  2omapen  16598  pw1mapen  16600