Theorem elex 2783

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1373  ∃wex 1515   ∈ wcel 2176  Vcvv 2772

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-v 2774

This theorem is referenced by:  elexi  2784  elexd  2785  elisset  2786  vtoclgft  2823  vtoclgf  2831  vtoclg1f  2832  vtocl2gf  2835  vtocl3gf  2836  spcimgft  2849  spcimegft  2851  elab4g  2922  elrabf  2927  mob  2955  sbcex  3007  sbcel1v  3061  sbcabel  3080  csbcomg  3116  csbvarg  3121  csbiebt  3133  csbnestgf  3146  csbidmg  3150  sbcco3g  3151  csbco3g  3152  eldif  3175  ssv  3215  elun  3314  elin  3356  elpwb  3626  snidb  3663  snssg  3767  dfopg  3817  eluni  3853  eliun  3931  csbexga  4172  nvel  4177  class2seteq  4207  axpweq  4215  snelpwi  4256  opexg  4272  elopab  4304  epelg  4337  elon2  4423  unexg  4490  reuhypd  4518  sucexg  4546  onsucb  4551  onsucelsucr  4556  sucunielr  4558  en2lp  4602  peano2  4643  peano2b  4663  opelvvg  4724  opeliunxp  4730  opeliunxp2  4818  ideqg  4829  elrnmptg  4930  imasng  5047  iniseg  5054  opswapg  5169  elxp4  5170  elxp5  5171  dmmptg  5180  iota2  5261  fnmpt  5402  fvexg  5595  fvelimab  5635  mptfvex  5665  fvmptdf  5667  fvmptdv2  5669  mpteqb  5670  fvmptt  5671  fvmptf  5672  fvopab6  5676  fsn2  5754  fmptpr  5776  eloprabga  6032  ovmpos  6069  ov2gf  6070  ovmpodxf  6071  ovmpox  6074  ovmpoga  6075  ovmpodf  6077  ovi3  6083  ovelrn  6095  suppssfv  6154  suppssov1  6155  offval3  6219  1stexg  6253  2ndexg  6254  elxp6  6255  elxp7  6256  releldm2  6271  fnmpo  6288  mpofvex  6291  mpoexg  6297  opeliunxp2f  6324  brtpos2  6337  rdgtfr  6460  rdgruledefgg  6461  frec0g  6483  sucinc2  6532  nntri3or  6579  relelec  6662  ecdmn0m  6664  mapvalg  6745  pmvalg  6746  elpmg  6751  elixp2  6789  mptelixpg  6821  elixpsn  6822  map1  6904  rex2dom  6910  mapdom1g  6944  mapxpen  6945  fival  7072  elfi2  7074  djulclr  7151  djurclr  7152  djulcl  7153  djurcl  7154  djulclb  7157  inl11  7167  djuss  7172  1stinl  7176  2ndinl  7177  1stinr  7178  2ndinr  7179  ismkvnex  7257  omniwomnimkv  7269  isacnm  7315  cc4n  7383  elinp  7587  addnqprlemfl  7672  addnqprlemfu  7673  mulnqprlemfl  7688  mulnqprlemfu  7689  recexprlemell  7735  recexprlemelu  7736  wrdexg  11005  wrdsymb0  11026  lswwrd  11040  ccatfvalfi  11048  swrdval  11101  swrd00g  11102  shftfvalg  11129  clim  11592  climmpt  11611  climshft2  11617  4sqlem2  12712  isstruct2r  12843  slotex  12859  setsvalg  12862  setsfun0  12868  setscom  12872  ressvalsets  12896  ressbasid  12902  restval  13077  topnvalg  13083  tgval  13094  ptex  13096  prdsex  13101  pwsval  13123  pwsbas  13124  pwselbasb  13125  pwssnf1o  13130  imasex  13137  qusex  13157  qusaddvallemg  13165  xpsfrnel2  13178  plusffvalg  13194  grpidvalg  13205  gsum0g  13228  sgrp1  13243  issubmnd  13274  pws0g  13283  issubm  13304  grppropstrg  13351  grpinvfvalg  13374  grpinvfng  13376  grpsubfvalg  13377  grpressid  13393  mulgfvalg  13457  mulgex  13459  mulgfng  13460  issubg  13509  subgex  13512  releqgg  13556  eqgex  13557  eqgfval  13558  isghm  13579  ablressid  13671  mgpvalg  13685  mgptopng  13691  rngressid  13716  rngpropd  13717  ringidvalg  13723  dfur2g  13724  issrg  13727  iscrng2  13777  ringressid  13825  opprvalg  13831  reldvdsrsrg  13854  dvdsrex  13860  unitgrp  13878  unitabl  13879  unitlinv  13888  unitrinv  13889  isnzr2  13946  issubrng  13961  issubrg  13983  subrgugrp  14002  aprap  14048  islmod  14053  scaffvalg  14068  lsssetm  14118  islssmg  14120  lspfval  14150  lspval  14152  lspcl  14153  lspex  14157  sraval  14199  rlmvalg  14216  rlmsubg  14220  rlmvnegg  14227  ixpsnbasval  14228  lidlvalg  14233  rspvalg  14234  lidlex  14235  rspex  14236  2idlvalg  14265  zrhvalg  14380  zlmval  14389  mplvalcoe  14452  mplbascoe  14453  mplplusgg  14465  toponsspwpwg  14494  eltg  14524  eltg2  14525  restbasg  14640  tgrest  14641  txvalex  14726  txval  14727  ispsmet  14795  ismet  14816  isxmet  14817  xmetunirn  14830  blfvalps  14857  vtxvalg  15615  iedgvalg  15616  bj-vtoclgft  15711  djucllem  15736  bj-nvel  15833  2omapen  15933