Theorem elex 2815

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

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

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 2213

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

This theorem is referenced by:  elexi  2816  elexd  2817  elisset  2818  vtoclgft  2855  vtoclgf  2863  vtoclg1f  2864  vtocl2gf  2867  vtocl3gf  2868  spcimgft  2883  spcimegft  2885  elab4g  2956  elrabf  2961  mob  2989  sbcex  3041  sbcel1v  3095  sbcabel  3115  csbcomg  3151  csbvarg  3156  csbiebt  3168  csbnestgf  3181  csbidmg  3185  sbcco3g  3186  csbco3g  3187  eldif  3210  ssv  3250  elun  3350  elin  3392  elif  3621  elpwb  3666  snidb  3703  eldifvsn  3810  snssg  3812  dfopg  3865  eluni  3901  eliun  3979  csbexga  4222  nvel  4227  class2seteq  4259  axpweq  4267  snelpwi  4309  opexg  4326  elopab  4358  epelg  4393  elon2  4479  unexg  4546  reuhypd  4574  sucexg  4602  onsucb  4607  onsucelsucr  4612  sucunielr  4614  en2lp  4658  peano2  4699  peano2b  4719  opelvvg  4781  opeliunxp  4787  opeliunxp2  4876  ideqg  4887  elrnmptg  4990  imasng  5108  iniseg  5115  opswapg  5230  elxp4  5231  elxp5  5232  dmmptg  5241  iota2  5323  fnmpt  5466  fvexg  5667  fvelimab  5711  mptfvex  5741  fvmptdf  5743  fvmptdv2  5745  mpteqb  5746  fvmptt  5747  fvmptf  5748  fvopab6  5752  fsn2  5829  fmptpr  5854  eloprabga  6118  ovmpos  6155  ov2gf  6156  ovmpodxf  6157  ovmpox  6160  ovmpoga  6161  ovmpodf  6163  ovi3  6169  ovelrn  6181  suppssov1  6241  offval3  6305  1stexg  6339  2ndexg  6340  elxp6  6341  elxp7  6342  releldm2  6357  fnmpo  6376  mpofvex  6379  mpoexg  6385  suppval  6415  opeliunxp2f  6447  brtpos2  6460  rdgtfr  6583  rdgruledefgg  6584  frec0g  6606  sucinc2  6657  nntri3or  6704  relelec  6787  ecdmn0m  6789  mapvalg  6870  pmvalg  6871  elpmg  6876  elixp2  6914  mptelixpg  6946  elixpsn  6947  map1  7030  rex2dom  7039  mapdom1g  7076  mapxpen  7077  fival  7212  elfi2  7214  djulclr  7291  djurclr  7292  djulcl  7293  djurcl  7294  djulclb  7297  inl11  7307  djuss  7312  1stinl  7316  2ndinl  7317  1stinr  7318  2ndinr  7319  ismkvnex  7397  omniwomnimkv  7409  isacnm  7461  cc4n  7533  elinp  7737  addnqprlemfl  7822  addnqprlemfu  7823  mulnqprlemfl  7838  mulnqprlemfu  7839  recexprlemell  7885  recexprlemelu  7886  wrdexg  11173  wrdsymb0  11195  lswwrd  11209  ccatfvalfi  11218  swrdval  11278  swrd00g  11279  pfxval  11304  cats1fvn  11394  cats1fvnd  11395  s2fv1g  11418  s2leng  11419  s2dmg  11420  shftfvalg  11441  clim  11904  climmpt  11923  climshft2  11929  4sqlem2  13025  isstruct2r  13156  slotex  13172  setsvalg  13175  setsfun0  13181  setscom  13185  ressvalsets  13210  ressbasid  13216  restval  13391  topnvalg  13397  tgval  13408  ptex  13410  prdsex  13415  pwsval  13437  pwsbas  13438  pwselbasb  13439  pwssnf1o  13444  imasex  13451  qusex  13471  qusaddvallemg  13479  xpsfrnel2  13492  plusffvalg  13508  grpidvalg  13519  gsum0g  13542  sgrp1  13557  issubmnd  13588  pws0g  13597  issubm  13618  grppropstrg  13665  grpinvfvalg  13688  grpinvfng  13690  grpsubfvalg  13691  grpressid  13707  mulgfvalg  13771  mulgex  13773  mulgfng  13774  issubg  13823  subgex  13826  releqgg  13870  eqgex  13871  eqgfval  13872  isghm  13893  ablressid  13985  mgpvalg  14000  mgptopng  14006  rngressid  14031  rngpropd  14032  ringidvalg  14038  dfur2g  14039  issrg  14042  iscrng2  14092  ringressid  14140  opprvalg  14146  dvdsrex  14176  unitgrp  14194  unitabl  14195  unitlinv  14204  unitrinv  14205  isnzr2  14262  issubrng  14277  issubrg  14299  subrgugrp  14318  aprap  14365  islmod  14370  scaffvalg  14385  lsssetm  14435  islssmg  14437  lspfval  14467  lspval  14469  lspcl  14470  lspex  14474  sraval  14516  rlmvalg  14533  rlmsubg  14537  rlmvnegg  14544  ixpsnbasval  14545  lidlvalg  14550  rspvalg  14551  lidlex  14552  rspex  14553  2idlvalg  14582  zrhvalg  14697  zlmval  14706  mplvalcoe  14774  mplbascoe  14775  mplplusgg  14787  toponsspwpwg  14816  eltg  14846  eltg2  14847  restbasg  14962  tgrest  14963  txvalex  15048  txval  15049  ispsmet  15117  ismet  15138  isxmet  15139  xmetunirn  15152  blfvalps  15179  vtxvalg  15940  iedgvalg  15941  vtxex  15942  edgvalg  15983  vtxdgfval  16212  wksfval  16246  iswlkg  16253  wlkvtxeledgg  16268  trlsfvalg  16307  clwwlkg  16317  clwwlkng  16329  eupthsg  16369  bj-vtoclgft  16476  djucllem  16501  bj-nvel  16596  2omapen  16699  pw1mapen  16701