Theorem elex 2811

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395  ∃wex 1538   ∈ wcel 2200  Vcvv 2799

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2801

This theorem is referenced by:  elexi  2812  elexd  2813  elisset  2814  vtoclgft  2851  vtoclgf  2859  vtoclg1f  2860  vtocl2gf  2863  vtocl3gf  2864  spcimgft  2879  spcimegft  2881  elab4g  2952  elrabf  2957  mob  2985  sbcex  3037  sbcel1v  3091  sbcabel  3111  csbcomg  3147  csbvarg  3152  csbiebt  3164  csbnestgf  3177  csbidmg  3181  sbcco3g  3182  csbco3g  3183  eldif  3206  ssv  3246  elun  3345  elin  3387  elif  3614  elpwb  3659  snidb  3696  snssg  3802  dfopg  3855  eluni  3891  eliun  3969  csbexga  4212  nvel  4217  class2seteq  4247  axpweq  4255  snelpwi  4297  opexg  4314  elopab  4346  epelg  4381  elon2  4467  unexg  4534  reuhypd  4562  sucexg  4590  onsucb  4595  onsucelsucr  4600  sucunielr  4602  en2lp  4646  peano2  4687  peano2b  4707  opelvvg  4768  opeliunxp  4774  opeliunxp2  4862  ideqg  4873  elrnmptg  4976  imasng  5093  iniseg  5100  opswapg  5215  elxp4  5216  elxp5  5217  dmmptg  5226  iota2  5308  fnmpt  5450  fvexg  5648  fvelimab  5692  mptfvex  5722  fvmptdf  5724  fvmptdv2  5726  mpteqb  5727  fvmptt  5728  fvmptf  5729  fvopab6  5733  fsn2  5811  fmptpr  5835  eloprabga  6097  ovmpos  6134  ov2gf  6135  ovmpodxf  6136  ovmpox  6139  ovmpoga  6140  ovmpodf  6142  ovi3  6148  ovelrn  6160  suppssfv  6220  suppssov1  6221  offval3  6285  1stexg  6319  2ndexg  6320  elxp6  6321  elxp7  6322  releldm2  6337  fnmpo  6354  mpofvex  6357  mpoexg  6363  opeliunxp2f  6390  brtpos2  6403  rdgtfr  6526  rdgruledefgg  6527  frec0g  6549  sucinc2  6600  nntri3or  6647  relelec  6730  ecdmn0m  6732  mapvalg  6813  pmvalg  6814  elpmg  6819  elixp2  6857  mptelixpg  6889  elixpsn  6890  map1  6973  rex2dom  6979  mapdom1g  7016  mapxpen  7017  fival  7148  elfi2  7150  djulclr  7227  djurclr  7228  djulcl  7229  djurcl  7230  djulclb  7233  inl11  7243  djuss  7248  1stinl  7252  2ndinl  7253  1stinr  7254  2ndinr  7255  ismkvnex  7333  omniwomnimkv  7345  isacnm  7396  cc4n  7468  elinp  7672  addnqprlemfl  7757  addnqprlemfu  7758  mulnqprlemfl  7773  mulnqprlemfu  7774  recexprlemell  7820  recexprlemelu  7821  wrdexg  11095  wrdsymb0  11117  lswwrd  11131  ccatfvalfi  11140  swrdval  11195  swrd00g  11196  pfxval  11221  cats1fvn  11311  cats1fvnd  11312  s2fv1g  11335  s2leng  11336  s2dmg  11337  shftfvalg  11344  clim  11807  climmpt  11826  climshft2  11832  4sqlem2  12927  isstruct2r  13058  slotex  13074  setsvalg  13077  setsfun0  13083  setscom  13087  ressvalsets  13112  ressbasid  13118  restval  13293  topnvalg  13299  tgval  13310  ptex  13312  prdsex  13317  pwsval  13339  pwsbas  13340  pwselbasb  13341  pwssnf1o  13346  imasex  13353  qusex  13373  qusaddvallemg  13381  xpsfrnel2  13394  plusffvalg  13410  grpidvalg  13421  gsum0g  13444  sgrp1  13459  issubmnd  13490  pws0g  13499  issubm  13520  grppropstrg  13567  grpinvfvalg  13590  grpinvfng  13592  grpsubfvalg  13593  grpressid  13609  mulgfvalg  13673  mulgex  13675  mulgfng  13676  issubg  13725  subgex  13728  releqgg  13772  eqgex  13773  eqgfval  13774  isghm  13795  ablressid  13887  mgpvalg  13901  mgptopng  13907  rngressid  13932  rngpropd  13933  ringidvalg  13939  dfur2g  13940  issrg  13943  iscrng2  13993  ringressid  14041  opprvalg  14047  dvdsrex  14077  unitgrp  14095  unitabl  14096  unitlinv  14105  unitrinv  14106  isnzr2  14163  issubrng  14178  issubrg  14200  subrgugrp  14219  aprap  14265  islmod  14270  scaffvalg  14285  lsssetm  14335  islssmg  14337  lspfval  14367  lspval  14369  lspcl  14370  lspex  14374  sraval  14416  rlmvalg  14433  rlmsubg  14437  rlmvnegg  14444  ixpsnbasval  14445  lidlvalg  14450  rspvalg  14451  lidlex  14452  rspex  14453  2idlvalg  14482  zrhvalg  14597  zlmval  14606  mplvalcoe  14669  mplbascoe  14670  mplplusgg  14682  toponsspwpwg  14711  eltg  14741  eltg2  14742  restbasg  14857  tgrest  14858  txvalex  14943  txval  14944  ispsmet  15012  ismet  15033  isxmet  15034  xmetunirn  15047  blfvalps  15074  vtxvalg  15832  iedgvalg  15833  vtxex  15834  edgvalg  15875  vtxdgfval  16047  wksfval  16063  iswlkg  16070  wlkvtxeledgg  16085  trlsfvalg  16122  clwwlkg  16131  bj-vtoclgft  16194  djucllem  16219  bj-nvel  16315  2omapen  16419  pw1mapen  16421