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  7320  djulclr  7390  djurclr  7391  djulcl  7392  djurcl  7393  djulclb  7396  inl11  7406  djuss  7411  1stinl  7415  2ndinl  7416  1stinr  7417  2ndinr  7418  ismkvnex  7496  omniwomnimkv  7508  isacnm  7560  cc4n  7638  elinp  7842  addnqprlemfl  7927  addnqprlemfu  7928  mulnqprlemfl  7943  mulnqprlemfu  7944  recexprlemell  7990  recexprlemelu  7991  indv  9298  hashmap  11284  wrdexg  11331  wrdsymb0  11353  lswwrd  11367  ccatfvalfi  11376  swrdval  11436  swrd00g  11437  pfxval  11462  cats1fvn  11552  cats1fvnd  11553  s2fv1g  11576  s2leng  11577  s2dmg  11578  shftfvalg  11599  clim  12066  climmpt  12085  climshft2  12091  4sqlem2  13191  ballotfilemsv  13305  isstruct2r  13415  slotex  13431  setsvalg  13434  setsfun0  13440  setscom  13444  ressvalsets  13470  ressbasid  13477  restval  13652  topnvalg  13658  tgval  13669  ptex  13671  imasex  13679  qusex  13699  qusaddvallemg  13707  xpsfrnel2  13720  plusffvalg  13735  grpidvalg  13746  gzsum0  13766  sgrp1  13779  issubmnd  13808  issubm  13832  grppropstrg  13877  grpinvfvalg  13900  grpinvfng  13902  grpsubfvalg  13903  grpressid  13919  mulgfvalg  13977  mulgex  13979  mulgfng  13980  issubg  14029  subgex  14032  releqgg  14076  eqgex  14077  eqgfval  14078  isghm  14099  cntzex  14144  cntzfval  14146  ablressid  14223  prdsex  14256  pwsval  14288  pwsbas  14289  pwselbasb  14290  pwssnf1o  14295  pws0g  14297  mgpvalg  14304  mgptopng  14312  rngressid  14337  rngpropd  14338  ringidvalg  14348  dfur2g  14350  issrg  14353  iscrng2  14403  ringressid  14452  opprvalg  14458  opprringb  14470  dvdsrex  14489  unitgrp  14507  unitabl  14508  unitlinv  14517  unitrinv  14518  isnzr2  14575  issubrng  14591  issubrg  14613  subrgugrp  14632  aprap  14682  aprprop  14685  islmod  14711  scaffvalg  14727  lsssetm  14777  islssmg  14779  lspfval  14809  lspval  14811  lspcl  14812  lspex  14816  sraval  14858  rlmvalg  14875  rlmsubg  14879  rlmvnegg  14886  ixpsnbasval  14887  lidlvalg  14892  rspvalg  14893  lidlex  14894  rspex  14895  2idlvalg  14924  zrhvalg  15037  zlmval  15046  aspval  15099  mplvalcoe  15172  mplbascoe  15173  mplplusgg  15185  toponsspwpwg  15214  eltg  15244  eltg2  15245  restbasg  15360  tgrest  15361  txvalex  15446  txval  15447  ispsmet  15515  ismet  15536  isxmet  15537  xmetunirn  15550  blfvalps  15577  vtxvalg  16423  iedgvalg  16424  vtxex  16425  edgvalg  16466  vtxdgfval  16695  wksfval  16729  iswlkg  16736  wlkvtxeledgg  16751  trlsfvalg  16790  clwwlkg  16800  clwwlkng  16812  eupthsg  16852  bj-vtoclgft  16969  djucllem  16994  bj-nvel  17089  pw1mapen  17192