Theorem elex 2833

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   = wceq 1402  ∃wex 1545   ∈ wcel 2209  Vcvv 2821

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is used by:  elexi  2834  elexd  2835  elisset  2836  vtoclgft  2873  vtoclgf  2881  vtoclg1f  2882  vtocl2gf  2885  vtocl3gf  2886  spcimgft  2901  spcimegft  2903  elab4g  2975  elrabf  2980  mob  3008  sbcex  3060  sbcel1v  3114  sbcabel  3134  csbcomg  3170  csbvarg  3175  csbiebt  3187  csbnestgf  3200  csbidmg  3204  sbcco3g  3205  csbco3g  3206  eldif  3229  ssv  3270  elun  3370  elin  3412  elif  3652  elpwb  3699  snidb  3739  eldifvsn  3847  snssg  3849  dfopg  3902  eluni  3938  eliun  4016  csbexga  4261  nvel  4266  class2seteq  4300  axpweq  4308  snelpwi  4351  opexg  4368  elopab  4400  epelg  4435  elon2  4521  unexg  4589  reuhypd  4617  sucexg  4645  onsucb  4650  onsucelsucr  4655  sucunielr  4657  en2lp  4701  peano2  4742  peano2b  4762  opelvvg  4824  opeliunxp  4830  opeliunxp2  4920  ideqg  4931  elrnmptg  5034  imasng  5152  iniseg  5159  opswapg  5274  elxp4  5275  elxp5  5276  dmmptg  5285  iota2  5367  fnmpt  5510  fvexg  5714  fvelimab  5759  mptfvex  5791  fvmptdf  5793  fvmptdv2  5795  mpteqb  5796  fvmptt  5797  fvmptf  5798  fvopab6  5805  fsn2  5882  fmptpr  5907  eloprabga  6175  ovmpos  6212  ov2gf  6213  ovmpodxf  6214  ovmpox  6217  ovmpoga  6218  ovmpodf  6220  ovi3  6226  ovelrn  6238  suppssov1  6299  offval3  6367  1stexg  6401  2ndexg  6402  elxp6  6403  elxp7  6404  releldm2  6419  fnmpo  6438  mpofvex  6441  mpoexg  6447  suppval  6477  opeliunxp2f  6509  brtpos2  6522  rdgtfr  6645  rdgruledefgg  6646  frec0g  6668  sucinc2  6719  nntri3or  6766  relelec  6849  ecdmn0m  6851  mapvalg  6932  pmvalg  6933  elpmg  6938  elixp2  6984  mptelixpg  7016  elixpsn  7017  map1  7101  rex2dom  7110  mapdom1g  7147  mapxpen  7148  fival  7304  elfi2  7306  2omapen  7319  djulclr  7389  djurclr  7390  djulcl  7391  djurcl  7392  djulclb  7395  inl11  7405  djuss  7410  1stinl  7414  2ndinl  7415  1stinr  7416  2ndinr  7417  ismkvnex  7495  omniwomnimkv  7507  isacnm  7559  cc4n  7637  elinp  7841  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemfl  7942  mulnqprlemfu  7943  recexprlemell  7989  recexprlemelu  7990  indv  9297  hashmap  11282  wrdexg  11329  wrdsymb0  11351  lswwrd  11365  ccatfvalfi  11374  swrdval  11434  swrd00g  11435  pfxval  11460  cats1fvn  11550  cats1fvnd  11551  s2fv1g  11574  s2leng  11575  s2dmg  11576  shftfvalg  11597  clim  12063  climmpt  12082  climshft2  12088  4sqlem2  13188  ballotfilemsv  13302  isstruct2r  13412  slotex  13428  setsvalg  13431  setsfun0  13437  setscom  13441  ressvalsets  13467  ressbasid  13473  restval  13648  topnvalg  13654  tgval  13665  ptex  13667  imasex  13675  qusex  13695  qusaddvallemg  13703  xpsfrnel2  13716  plusffvalg  13731  grpidvalg  13742  gzsum0  13762  sgrp1  13775  issubmnd  13804  issubm  13828  grppropstrg  13873  grpinvfvalg  13896  grpinvfng  13898  grpsubfvalg  13899  grpressid  13915  mulgfvalg  13973  mulgex  13975  mulgfng  13976  issubg  14025  subgex  14028  releqgg  14072  eqgex  14073  eqgfval  14074  isghm  14095  ablressid  14188  prdsex  14221  pwsval  14253  pwsbas  14254  pwselbasb  14255  pwssnf1o  14260  pws0g  14262  mgpvalg  14269  mgptopng  14277  rngressid  14302  rngpropd  14303  ringidvalg  14313  dfur2g  14315  issrg  14318  iscrng2  14368  ringressid  14417  opprvalg  14423  opprringb  14435  dvdsrex  14454  unitgrp  14472  unitabl  14473  unitlinv  14482  unitrinv  14483  isnzr2  14540  issubrng  14556  issubrg  14578  subrgugrp  14597  aprap  14647  aprprop  14650  islmod  14676  scaffvalg  14692  lsssetm  14742  islssmg  14744  lspfval  14774  lspval  14776  lspcl  14777  lspex  14781  sraval  14823  rlmvalg  14840  rlmsubg  14844  rlmvnegg  14851  ixpsnbasval  14852  lidlvalg  14857  rspvalg  14858  lidlex  14859  rspex  14860  2idlvalg  14889  zrhvalg  15002  zlmval  15011  aspval  15064  mplvalcoe  15130  mplbascoe  15131  mplplusgg  15143  toponsspwpwg  15172  eltg  15202  eltg2  15203  restbasg  15318  tgrest  15319  txvalex  15404  txval  15405  ispsmet  15473  ismet  15494  isxmet  15495  xmetunirn  15508  blfvalps  15535  vtxvalg  16355  iedgvalg  16356  vtxex  16357  edgvalg  16398  vtxdgfval  16627  wksfval  16661  iswlkg  16668  wlkvtxeledgg  16683  trlsfvalg  16722  clwwlkg  16732  clwwlkng  16744  eupthsg  16784  bj-vtoclgft  16901  djucllem  16926  bj-nvel  17021  pw1mapen  17124