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  11128  wrdsymb0  11150  lswwrd  11164  ccatfvalfi  11173  swrdval  11233  swrd00g  11234  pfxval  11259  cats1fvn  11349  cats1fvnd  11350  s2fv1g  11373  s2leng  11374  s2dmg  11375  shftfvalg  11383  clim  11846  climmpt  11865  climshft2  11871  4sqlem2  12967  isstruct2r  13098  slotex  13114  setsvalg  13117  setsfun0  13123  setscom  13127  ressvalsets  13152  ressbasid  13158  restval  13333  topnvalg  13339  tgval  13350  ptex  13352  prdsex  13357  pwsval  13379  pwsbas  13380  pwselbasb  13381  pwssnf1o  13386  imasex  13393  qusex  13413  qusaddvallemg  13421  xpsfrnel2  13434  plusffvalg  13450  grpidvalg  13461  gsum0g  13484  sgrp1  13499  issubmnd  13530  pws0g  13539  issubm  13560  grppropstrg  13607  grpinvfvalg  13630  grpinvfng  13632  grpsubfvalg  13633  grpressid  13649  mulgfvalg  13713  mulgex  13715  mulgfng  13716  issubg  13765  subgex  13768  releqgg  13812  eqgex  13813  eqgfval  13814  isghm  13835  ablressid  13927  mgpvalg  13942  mgptopng  13948  rngressid  13973  rngpropd  13974  ringidvalg  13980  dfur2g  13981  issrg  13984  iscrng2  14034  ringressid  14082  opprvalg  14088  dvdsrex  14118  unitgrp  14136  unitabl  14137  unitlinv  14146  unitrinv  14147  isnzr2  14204  issubrng  14219  issubrg  14241  subrgugrp  14260  aprap  14306  islmod  14311  scaffvalg  14326  lsssetm  14376  islssmg  14378  lspfval  14408  lspval  14410  lspcl  14411  lspex  14415  sraval  14457  rlmvalg  14474  rlmsubg  14478  rlmvnegg  14485  ixpsnbasval  14486  lidlvalg  14491  rspvalg  14492  lidlex  14493  rspex  14494  2idlvalg  14523  zrhvalg  14638  zlmval  14647  mplvalcoe  14710  mplbascoe  14711  mplplusgg  14723  toponsspwpwg  14752  eltg  14782  eltg2  14783  restbasg  14898  tgrest  14899  txvalex  14984  txval  14985  ispsmet  15053  ismet  15074  isxmet  15075  xmetunirn  15088  blfvalps  15115  vtxvalg  15873  iedgvalg  15874  vtxex  15875  edgvalg  15916  vtxdgfval  16145  wksfval  16179  iswlkg  16186  wlkvtxeledgg  16201  trlsfvalg  16240  clwwlkg  16250  clwwlkng  16262  eupthsg  16302  bj-vtoclgft  16397  djucllem  16422  bj-nvel  16518  2omapen  16621  pw1mapen  16623