Theorem elex 2762

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1363  ∃wex 1502   ∈ wcel 2159  Vcvv 2751

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-ext 2170

This theorem depends on definitions:  df-bi 117  df-sb 1773  df-clab 2175  df-cleq 2181  df-clel 2184  df-v 2753

This theorem is referenced by:  elexi  2763  elexd  2764  elisset  2765  vtoclgft  2801  vtoclgf  2809  vtoclg1f  2810  vtocl2gf  2813  vtocl3gf  2814  spcimgft  2827  spcimegft  2829  elab4g  2900  elrabf  2905  mob  2933  sbcex  2985  sbcel1v  3039  sbcabel  3058  csbcomg  3094  csbvarg  3099  csbiebt  3110  csbnestgf  3123  csbidmg  3127  sbcco3g  3128  csbco3g  3129  eldif  3152  ssv  3191  elun  3290  elin  3332  elpwb  3599  snidb  3636  snssg  3740  dfopg  3790  eluni  3826  eliun  3904  csbexga  4145  nvel  4150  class2seteq  4177  axpweq  4185  snelpwi  4226  opexg  4242  elopab  4272  epelg  4304  elon2  4390  unexg  4457  reuhypd  4485  sucexg  4511  onsucb  4516  onsucelsucr  4521  sucunielr  4523  en2lp  4567  peano2  4608  peano2b  4628  opelvvg  4689  opeliunxp  4695  opeliunxp2  4781  ideqg  4792  elrnmptg  4893  imasng  5007  iniseg  5014  opswapg  5129  elxp4  5130  elxp5  5131  dmmptg  5140  iota2  5220  fnmpt  5356  fvexg  5548  fvelimab  5587  mptfvex  5616  fvmptdf  5618  fvmptdv2  5620  mpteqb  5621  fvmptt  5622  fvmptf  5623  fvopab6  5627  fsn2  5705  fmptpr  5723  eloprabga  5977  ovmpos  6014  ov2gf  6015  ovmpodxf  6016  ovmpox  6019  ovmpoga  6020  ovmpodf  6022  ovi3  6027  ovelrn  6039  suppssfv  6096  suppssov1  6097  offval3  6152  1stexg  6185  2ndexg  6186  elxp6  6187  elxp7  6188  releldm2  6203  fnmpo  6220  mpofvex  6221  mpoexg  6229  opeliunxp2f  6256  brtpos2  6269  rdgtfr  6392  rdgruledefgg  6393  frec0g  6415  sucinc2  6464  nntri3or  6511  relelec  6592  ecdmn0m  6594  mapvalg  6675  pmvalg  6676  elpmg  6681  elixp2  6719  mptelixpg  6751  elixpsn  6752  map1  6829  mapdom1g  6864  mapxpen  6865  fival  6986  elfi2  6988  djulclr  7065  djurclr  7066  djulcl  7067  djurcl  7068  djulclb  7071  inl11  7081  djuss  7086  1stinl  7090  2ndinl  7091  1stinr  7092  2ndinr  7093  ismkvnex  7170  omniwomnimkv  7182  cc4n  7287  elinp  7490  addnqprlemfl  7575  addnqprlemfu  7576  mulnqprlemfl  7591  mulnqprlemfu  7592  recexprlemell  7638  recexprlemelu  7639  shftfvalg  10844  clim  11306  climmpt  11325  climshft2  11331  4sqlem2  12404  isstruct2r  12490  slotex  12506  setsvalg  12509  setsfun0  12515  setscom  12519  ressvalsets  12541  ressbasid  12547  restval  12715  topnvalg  12721  tgval  12732  ptex  12734  prdsex  12739  imasex  12747  qusex  12767  qusaddvallemg  12774  xpsfrnel2  12787  plusffvalg  12803  grpidvalg  12814  sgrp1  12839  issubmnd  12868  issubm  12889  grppropstrg  12929  grpinvfvalg  12951  grpinvfng  12953  grpsubfvalg  12954  grpressid  12970  mulgfvalg  13028  mulgex  13030  mulgfng  13031  issubg  13077  subgex  13080  releqgg  13124  eqgex  13125  eqgfval  13126  isghm  13142  ablressid  13232  mgpvalg  13237  mgptopng  13243  rngressid  13268  rngpropd  13269  ringidvalg  13275  dfur2g  13276  issrg  13279  iscrng2  13329  ringressid  13373  opprvalg  13379  reldvdsrsrg  13402  dvdsrex  13408  unitgrp  13426  unitabl  13427  unitlinv  13436  unitrinv  13437  issubrng  13506  issubrg  13528  subrgugrp  13547  aprap  13562  islmod  13567  scaffvalg  13582  lsssetm  13632  islssmg  13634  lspfval  13664  lspval  13666  lspcl  13667  lspex  13671  sraval  13713  rlmvalg  13730  rlmsubg  13734  rlmvnegg  13741  ixpsnbasval  13742  lidlvalg  13747  rspvalg  13748  lidlex  13749  rspex  13750  2idlvalg  13777  zlmval  13872  toponsspwpwg  13905  eltg  13935  eltg2  13936  restbasg  14051  tgrest  14052  txvalex  14137  txval  14138  ispsmet  14206  ismet  14227  isxmet  14228  xmetunirn  14241  blfvalps  14268  bj-vtoclgft  14910  djucllem  14935  bj-nvel  15032