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  3801  dfopg  3854  eluni  3890  eliun  3968  csbexga  4211  nvel  4216  class2seteq  4246  axpweq  4254  snelpwi  4296  opexg  4313  elopab  4345  epelg  4380  elon2  4466  unexg  4533  reuhypd  4561  sucexg  4589  onsucb  4594  onsucelsucr  4599  sucunielr  4601  en2lp  4645  peano2  4686  peano2b  4706  opelvvg  4767  opeliunxp  4773  opeliunxp2  4861  ideqg  4872  elrnmptg  4975  imasng  5092  iniseg  5099  opswapg  5214  elxp4  5215  elxp5  5216  dmmptg  5225  iota2  5307  fnmpt  5449  fvexg  5645  fvelimab  5689  mptfvex  5719  fvmptdf  5721  fvmptdv2  5723  mpteqb  5724  fvmptt  5725  fvmptf  5726  fvopab6  5730  fsn2  5808  fmptpr  5830  eloprabga  6090  ovmpos  6127  ov2gf  6128  ovmpodxf  6129  ovmpox  6132  ovmpoga  6133  ovmpodf  6135  ovi3  6141  ovelrn  6153  suppssfv  6212  suppssov1  6213  offval3  6277  1stexg  6311  2ndexg  6312  elxp6  6313  elxp7  6314  releldm2  6329  fnmpo  6346  mpofvex  6349  mpoexg  6355  opeliunxp2f  6382  brtpos2  6395  rdgtfr  6518  rdgruledefgg  6519  frec0g  6541  sucinc2  6590  nntri3or  6637  relelec  6720  ecdmn0m  6722  mapvalg  6803  pmvalg  6804  elpmg  6809  elixp2  6847  mptelixpg  6879  elixpsn  6880  map1  6963  rex2dom  6969  mapdom1g  7004  mapxpen  7005  fival  7133  elfi2  7135  djulclr  7212  djurclr  7213  djulcl  7214  djurcl  7215  djulclb  7218  inl11  7228  djuss  7233  1stinl  7237  2ndinl  7238  1stinr  7239  2ndinr  7240  ismkvnex  7318  omniwomnimkv  7330  isacnm  7381  cc4n  7453  elinp  7657  addnqprlemfl  7742  addnqprlemfu  7743  mulnqprlemfl  7758  mulnqprlemfu  7759  recexprlemell  7805  recexprlemelu  7806  wrdexg  11077  wrdsymb0  11099  lswwrd  11113  ccatfvalfi  11122  swrdval  11175  swrd00g  11176  pfxval  11201  cats1fvn  11291  cats1fvnd  11292  s2fv1g  11315  s2leng  11316  s2dmg  11317  shftfvalg  11324  clim  11787  climmpt  11806  climshft2  11812  4sqlem2  12907  isstruct2r  13038  slotex  13054  setsvalg  13057  setsfun0  13063  setscom  13067  ressvalsets  13092  ressbasid  13098  restval  13273  topnvalg  13279  tgval  13290  ptex  13292  prdsex  13297  pwsval  13319  pwsbas  13320  pwselbasb  13321  pwssnf1o  13326  imasex  13333  qusex  13353  qusaddvallemg  13361  xpsfrnel2  13374  plusffvalg  13390  grpidvalg  13401  gsum0g  13424  sgrp1  13439  issubmnd  13470  pws0g  13479  issubm  13500  grppropstrg  13547  grpinvfvalg  13570  grpinvfng  13572  grpsubfvalg  13573  grpressid  13589  mulgfvalg  13653  mulgex  13655  mulgfng  13656  issubg  13705  subgex  13708  releqgg  13752  eqgex  13753  eqgfval  13754  isghm  13775  ablressid  13867  mgpvalg  13881  mgptopng  13887  rngressid  13912  rngpropd  13913  ringidvalg  13919  dfur2g  13920  issrg  13923  iscrng2  13973  ringressid  14021  opprvalg  14027  reldvdsrsrg  14050  dvdsrex  14056  unitgrp  14074  unitabl  14075  unitlinv  14084  unitrinv  14085  isnzr2  14142  issubrng  14157  issubrg  14179  subrgugrp  14198  aprap  14244  islmod  14249  scaffvalg  14264  lsssetm  14314  islssmg  14316  lspfval  14346  lspval  14348  lspcl  14349  lspex  14353  sraval  14395  rlmvalg  14412  rlmsubg  14416  rlmvnegg  14423  ixpsnbasval  14424  lidlvalg  14429  rspvalg  14430  lidlex  14431  rspex  14432  2idlvalg  14461  zrhvalg  14576  zlmval  14585  mplvalcoe  14648  mplbascoe  14649  mplplusgg  14661  toponsspwpwg  14690  eltg  14720  eltg2  14721  restbasg  14836  tgrest  14837  txvalex  14922  txval  14923  ispsmet  14991  ismet  15012  isxmet  15013  xmetunirn  15026  blfvalps  15053  vtxvalg  15811  iedgvalg  15812  vtxex  15813  edgvalg  15854  wksfval  16028  iswlkg  16032  wlkvtxeledgg  16041  bj-vtoclgft  16097  djucllem  16122  bj-nvel  16218  2omapen  16319  pw1mapen  16321