Theorem elex 2750

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1353  ∃wex 1492   ∈ wcel 2148  Vcvv 2739

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2741

This theorem is referenced by:  elexi  2751  elexd  2752  elisset  2753  vtoclgft  2789  vtoclgf  2797  vtoclg1f  2798  vtocl2gf  2801  vtocl3gf  2802  spcimgft  2815  spcimegft  2817  elab4g  2888  elrabf  2893  mob  2921  sbcex  2973  sbcel1v  3027  sbcabel  3046  csbcomg  3082  csbvarg  3087  csbiebt  3098  csbnestgf  3111  csbidmg  3115  sbcco3g  3116  csbco3g  3117  eldif  3140  ssv  3179  elun  3278  elin  3320  elpwb  3587  snidb  3624  snssg  3728  dfopg  3778  eluni  3814  eliun  3892  csbexga  4133  nvel  4138  class2seteq  4165  axpweq  4173  snelpwi  4214  opexg  4230  elopab  4260  epelg  4292  elon2  4378  unexg  4445  reuhypd  4473  sucexg  4499  onsucb  4504  onsucelsucr  4509  sucunielr  4511  en2lp  4555  peano2  4596  peano2b  4616  opelvvg  4677  opeliunxp  4683  opeliunxp2  4769  ideqg  4780  elrnmptg  4881  imasng  4995  iniseg  5002  opswapg  5117  elxp4  5118  elxp5  5119  dmmptg  5128  iota2  5208  fnmpt  5344  fvexg  5536  fvelimab  5574  mptfvex  5603  fvmptdf  5605  fvmptdv2  5607  mpteqb  5608  fvmptt  5609  fvmptf  5610  fvopab6  5614  fsn2  5692  fmptpr  5710  eloprabga  5964  ovmpos  6000  ov2gf  6001  ovmpodxf  6002  ovmpox  6005  ovmpoga  6006  ovmpodf  6008  ovi3  6013  ovelrn  6025  suppssfv  6081  suppssov1  6082  offval3  6137  1stexg  6170  2ndexg  6171  elxp6  6172  elxp7  6173  releldm2  6188  fnmpo  6205  mpofvex  6206  mpoexg  6214  opeliunxp2f  6241  brtpos2  6254  rdgtfr  6377  rdgruledefgg  6378  frec0g  6400  sucinc2  6449  nntri3or  6496  relelec  6577  ecdmn0m  6579  mapvalg  6660  pmvalg  6661  elpmg  6666  elixp2  6704  mptelixpg  6736  elixpsn  6737  map1  6814  mapdom1g  6849  mapxpen  6850  fival  6971  elfi2  6973  djulclr  7050  djurclr  7051  djulcl  7052  djurcl  7053  djulclb  7056  inl11  7066  djuss  7071  1stinl  7075  2ndinl  7076  1stinr  7077  2ndinr  7078  ismkvnex  7155  omniwomnimkv  7167  cc4n  7272  elinp  7475  addnqprlemfl  7560  addnqprlemfu  7561  mulnqprlemfl  7576  mulnqprlemfu  7577  recexprlemell  7623  recexprlemelu  7624  shftfvalg  10829  clim  11291  climmpt  11310  climshft2  11316  4sqlem2  12389  isstruct2r  12475  slotex  12491  setsvalg  12494  setsfun0  12500  setscom  12504  ressvalsets  12526  restval  12699  topnvalg  12705  tgval  12716  ptex  12718  prdsex  12723  imasex  12731  qusaddvallemg  12757  xpsfrnel2  12770  plusffvalg  12786  grpidvalg  12797  sgrp1  12821  issubmnd  12848  issubm  12868  grppropstrg  12900  grpinvfvalg  12920  grpinvfng  12922  grpsubfvalg  12923  grpressid  12936  mulgfvalg  12990  mulgfng  12992  issubg  13038  subgex  13041  releqgg  13085  eqgfval  13086  mgpvalg  13138  mgptopng  13144  ringidvalg  13149  dfur2g  13150  issrg  13153  iscrng2  13203  ringressid  13243  opprvalg  13246  reldvdsrsrg  13266  dvdsrex  13272  unitgrp  13290  unitabl  13291  unitlinv  13300  unitrinv  13301  issubrg  13347  subrgugrp  13366  aprap  13381  islmod  13386  scaffvalg  13401  lsssetm  13449  islssm  13450  toponsspwpwg  13561  eltg  13591  eltg2  13592  restbasg  13707  tgrest  13708  txvalex  13793  txval  13794  ispsmet  13862  ismet  13883  isxmet  13884  xmetunirn  13897  blfvalps  13924  bj-vtoclgft  14566  djucllem  14591  bj-nvel  14688