Theorem elex 2782

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1372  ∃wex 1514   ∈ wcel 2175  Vcvv 2771

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-v 2773

This theorem is referenced by:  elexi  2783  elexd  2784  elisset  2785  vtoclgft  2822  vtoclgf  2830  vtoclg1f  2831  vtocl2gf  2834  vtocl3gf  2835  spcimgft  2848  spcimegft  2850  elab4g  2921  elrabf  2926  mob  2954  sbcex  3006  sbcel1v  3060  sbcabel  3079  csbcomg  3115  csbvarg  3120  csbiebt  3132  csbnestgf  3145  csbidmg  3149  sbcco3g  3150  csbco3g  3151  eldif  3174  ssv  3214  elun  3313  elin  3355  elpwb  3625  snidb  3662  snssg  3766  dfopg  3816  eluni  3852  eliun  3930  csbexga  4171  nvel  4176  class2seteq  4206  axpweq  4214  snelpwi  4255  opexg  4271  elopab  4303  epelg  4336  elon2  4422  unexg  4489  reuhypd  4517  sucexg  4545  onsucb  4550  onsucelsucr  4555  sucunielr  4557  en2lp  4601  peano2  4642  peano2b  4662  opelvvg  4723  opeliunxp  4729  opeliunxp2  4817  ideqg  4828  elrnmptg  4929  imasng  5046  iniseg  5053  opswapg  5168  elxp4  5169  elxp5  5170  dmmptg  5179  iota2  5260  fnmpt  5401  fvexg  5594  fvelimab  5634  mptfvex  5664  fvmptdf  5666  fvmptdv2  5668  mpteqb  5669  fvmptt  5670  fvmptf  5671  fvopab6  5675  fsn2  5753  fmptpr  5775  eloprabga  6031  ovmpos  6068  ov2gf  6069  ovmpodxf  6070  ovmpox  6073  ovmpoga  6074  ovmpodf  6076  ovi3  6082  ovelrn  6094  suppssfv  6153  suppssov1  6154  offval3  6218  1stexg  6252  2ndexg  6253  elxp6  6254  elxp7  6255  releldm2  6270  fnmpo  6287  mpofvex  6290  mpoexg  6296  opeliunxp2f  6323  brtpos2  6336  rdgtfr  6459  rdgruledefgg  6460  frec0g  6482  sucinc2  6531  nntri3or  6578  relelec  6661  ecdmn0m  6663  mapvalg  6744  pmvalg  6745  elpmg  6750  elixp2  6788  mptelixpg  6820  elixpsn  6821  map1  6903  rex2dom  6909  mapdom1g  6943  mapxpen  6944  fival  7071  elfi2  7073  djulclr  7150  djurclr  7151  djulcl  7152  djurcl  7153  djulclb  7156  inl11  7166  djuss  7171  1stinl  7175  2ndinl  7176  1stinr  7177  2ndinr  7178  ismkvnex  7256  omniwomnimkv  7268  isacnm  7314  cc4n  7382  elinp  7586  addnqprlemfl  7671  addnqprlemfu  7672  mulnqprlemfl  7687  mulnqprlemfu  7688  recexprlemell  7734  recexprlemelu  7735  wrdexg  11003  wrdsymb0  11024  lswwrd  11038  ccatfvalfi  11046  shftfvalg  11100  clim  11563  climmpt  11582  climshft2  11588  4sqlem2  12683  isstruct2r  12814  slotex  12830  setsvalg  12833  setsfun0  12839  setscom  12843  ressvalsets  12867  ressbasid  12873  restval  13048  topnvalg  13054  tgval  13065  ptex  13067  prdsex  13072  pwsval  13094  pwsbas  13095  pwselbasb  13096  pwssnf1o  13101  imasex  13108  qusex  13128  qusaddvallemg  13136  xpsfrnel2  13149  plusffvalg  13165  grpidvalg  13176  gsum0g  13199  sgrp1  13214  issubmnd  13245  pws0g  13254  issubm  13275  grppropstrg  13322  grpinvfvalg  13345  grpinvfng  13347  grpsubfvalg  13348  grpressid  13364  mulgfvalg  13428  mulgex  13430  mulgfng  13431  issubg  13480  subgex  13483  releqgg  13527  eqgex  13528  eqgfval  13529  isghm  13550  ablressid  13642  mgpvalg  13656  mgptopng  13662  rngressid  13687  rngpropd  13688  ringidvalg  13694  dfur2g  13695  issrg  13698  iscrng2  13748  ringressid  13796  opprvalg  13802  reldvdsrsrg  13825  dvdsrex  13831  unitgrp  13849  unitabl  13850  unitlinv  13859  unitrinv  13860  isnzr2  13917  issubrng  13932  issubrg  13954  subrgugrp  13973  aprap  14019  islmod  14024  scaffvalg  14039  lsssetm  14089  islssmg  14091  lspfval  14121  lspval  14123  lspcl  14124  lspex  14128  sraval  14170  rlmvalg  14187  rlmsubg  14191  rlmvnegg  14198  ixpsnbasval  14199  lidlvalg  14204  rspvalg  14205  lidlex  14206  rspex  14207  2idlvalg  14236  zrhvalg  14351  zlmval  14360  mplvalcoe  14423  mplbascoe  14424  mplplusgg  14436  toponsspwpwg  14465  eltg  14495  eltg2  14496  restbasg  14611  tgrest  14612  txvalex  14697  txval  14698  ispsmet  14766  ismet  14787  isxmet  14788  xmetunirn  14801  blfvalps  14828  vtxvalg  15586  iedgvalg  15587  bj-vtoclgft  15673  djucllem  15698  bj-nvel  15795  2omapen  15895