Theorem elex 2774

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364  ∃wex 1506   ∈ wcel 2167  Vcvv 2763

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765

This theorem is referenced by:  elexi  2775  elexd  2776  elisset  2777  vtoclgft  2814  vtoclgf  2822  vtoclg1f  2823  vtocl2gf  2826  vtocl3gf  2827  spcimgft  2840  spcimegft  2842  elab4g  2913  elrabf  2918  mob  2946  sbcex  2998  sbcel1v  3052  sbcabel  3071  csbcomg  3107  csbvarg  3112  csbiebt  3124  csbnestgf  3137  csbidmg  3141  sbcco3g  3142  csbco3g  3143  eldif  3166  ssv  3206  elun  3305  elin  3347  elpwb  3616  snidb  3653  snssg  3757  dfopg  3807  eluni  3843  eliun  3921  csbexga  4162  nvel  4167  class2seteq  4197  axpweq  4205  snelpwi  4246  opexg  4262  elopab  4293  epelg  4326  elon2  4412  unexg  4479  reuhypd  4507  sucexg  4535  onsucb  4540  onsucelsucr  4545  sucunielr  4547  en2lp  4591  peano2  4632  peano2b  4652  opelvvg  4713  opeliunxp  4719  opeliunxp2  4807  ideqg  4818  elrnmptg  4919  imasng  5035  iniseg  5042  opswapg  5157  elxp4  5158  elxp5  5159  dmmptg  5168  iota2  5249  fnmpt  5387  fvexg  5580  fvelimab  5620  mptfvex  5650  fvmptdf  5652  fvmptdv2  5654  mpteqb  5655  fvmptt  5656  fvmptf  5657  fvopab6  5661  fsn2  5739  fmptpr  5757  eloprabga  6013  ovmpos  6050  ov2gf  6051  ovmpodxf  6052  ovmpox  6055  ovmpoga  6056  ovmpodf  6058  ovi3  6064  ovelrn  6076  suppssfv  6135  suppssov1  6136  offval3  6200  1stexg  6234  2ndexg  6235  elxp6  6236  elxp7  6237  releldm2  6252  fnmpo  6269  mpofvex  6272  mpoexg  6278  opeliunxp2f  6305  brtpos2  6318  rdgtfr  6441  rdgruledefgg  6442  frec0g  6464  sucinc2  6513  nntri3or  6560  relelec  6643  ecdmn0m  6645  mapvalg  6726  pmvalg  6727  elpmg  6732  elixp2  6770  mptelixpg  6802  elixpsn  6803  map1  6880  mapdom1g  6917  mapxpen  6918  fival  7045  elfi2  7047  djulclr  7124  djurclr  7125  djulcl  7126  djurcl  7127  djulclb  7130  inl11  7140  djuss  7145  1stinl  7149  2ndinl  7150  1stinr  7151  2ndinr  7152  ismkvnex  7230  omniwomnimkv  7242  isacnm  7288  cc4n  7356  elinp  7560  addnqprlemfl  7645  addnqprlemfu  7646  mulnqprlemfl  7661  mulnqprlemfu  7662  recexprlemell  7708  recexprlemelu  7709  wrdexg  10965  wrdsymb0  10986  shftfvalg  11002  clim  11465  climmpt  11484  climshft2  11490  4sqlem2  12585  isstruct2r  12716  slotex  12732  setsvalg  12735  setsfun0  12741  setscom  12745  ressvalsets  12769  ressbasid  12775  restval  12949  topnvalg  12955  tgval  12966  ptex  12968  prdsex  12973  pwsval  12995  pwsbas  12996  pwselbasb  12997  pwssnf1o  13002  imasex  13009  qusex  13029  qusaddvallemg  13037  xpsfrnel2  13050  plusffvalg  13066  grpidvalg  13077  gsum0g  13100  sgrp1  13115  issubmnd  13146  pws0g  13155  issubm  13176  grppropstrg  13223  grpinvfvalg  13246  grpinvfng  13248  grpsubfvalg  13249  grpressid  13265  mulgfvalg  13329  mulgex  13331  mulgfng  13332  issubg  13381  subgex  13384  releqgg  13428  eqgex  13429  eqgfval  13430  isghm  13451  ablressid  13543  mgpvalg  13557  mgptopng  13563  rngressid  13588  rngpropd  13589  ringidvalg  13595  dfur2g  13596  issrg  13599  iscrng2  13649  ringressid  13697  opprvalg  13703  reldvdsrsrg  13726  dvdsrex  13732  unitgrp  13750  unitabl  13751  unitlinv  13760  unitrinv  13761  isnzr2  13818  issubrng  13833  issubrg  13855  subrgugrp  13874  aprap  13920  islmod  13925  scaffvalg  13940  lsssetm  13990  islssmg  13992  lspfval  14022  lspval  14024  lspcl  14025  lspex  14029  sraval  14071  rlmvalg  14088  rlmsubg  14092  rlmvnegg  14099  ixpsnbasval  14100  lidlvalg  14105  rspvalg  14106  lidlex  14107  rspex  14108  2idlvalg  14137  zrhvalg  14252  zlmval  14261  mplvalcoe  14324  mplbascoe  14325  mplplusgg  14337  toponsspwpwg  14366  eltg  14396  eltg2  14397  restbasg  14512  tgrest  14513  txvalex  14598  txval  14599  ispsmet  14667  ismet  14688  isxmet  14689  xmetunirn  14702  blfvalps  14729  bj-vtoclgft  15529  djucllem  15554  bj-nvel  15651  2omapen  15751