Theorem elex 2748

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 2743	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4	1, 2, 3	3imtr4i 201	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)

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

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 2739

This theorem is referenced by:  elexi  2749  elexd  2750  elisset  2751  vtoclgft  2787  vtoclgf  2795  vtoclg1f  2796  vtocl2gf  2799  vtocl3gf  2800  spcimgft  2813  spcimegft  2815  elab4g  2886  elrabf  2891  mob  2919  sbcex  2971  sbcel1v  3025  sbcabel  3044  csbcomg  3080  csbvarg  3085  csbiebt  3096  csbnestgf  3109  csbidmg  3113  sbcco3g  3114  csbco3g  3115  eldif  3138  ssv  3177  elun  3276  elin  3318  elpwb  3585  snidb  3622  snssg  3726  dfopg  3775  eluni  3811  eliun  3889  csbexga  4129  nvel  4134  class2seteq  4161  axpweq  4169  snelpwi  4210  opexg  4226  elopab  4256  epelg  4288  elon2  4374  unexg  4441  reuhypd  4469  sucexg  4495  onsucb  4500  onsucelsucr  4505  sucunielr  4507  en2lp  4551  peano2  4592  peano2b  4612  opelvvg  4673  opeliunxp  4679  opeliunxp2  4764  ideqg  4775  elrnmptg  4876  imasng  4990  iniseg  4997  opswapg  5112  elxp4  5113  elxp5  5114  dmmptg  5123  iota2  5203  fnmpt  5339  fvexg  5531  fvelimab  5569  mptfvex  5598  fvmptdf  5600  fvmptdv2  5602  mpteqb  5603  fvmptt  5604  fvmptf  5605  fvopab6  5609  fsn2  5687  fmptpr  5705  eloprabga  5957  ovmpos  5993  ov2gf  5994  ovmpodxf  5995  ovmpox  5998  ovmpoga  5999  ovmpodf  6001  ovi3  6006  ovelrn  6018  suppssfv  6074  suppssov1  6075  offval3  6130  1stexg  6163  2ndexg  6164  elxp6  6165  elxp7  6166  releldm2  6181  fnmpo  6198  mpofvex  6199  mpoexg  6207  opeliunxp2f  6234  brtpos2  6247  rdgtfr  6370  rdgruledefgg  6371  frec0g  6393  sucinc2  6442  nntri3or  6489  relelec  6570  ecdmn0m  6572  mapvalg  6653  pmvalg  6654  elpmg  6659  elixp2  6697  mptelixpg  6729  elixpsn  6730  map1  6807  mapdom1g  6842  mapxpen  6843  fival  6964  elfi2  6966  djulclr  7043  djurclr  7044  djulcl  7045  djurcl  7046  djulclb  7049  inl11  7059  djuss  7064  1stinl  7068  2ndinl  7069  1stinr  7070  2ndinr  7071  ismkvnex  7148  omniwomnimkv  7160  cc4n  7265  elinp  7468  addnqprlemfl  7553  addnqprlemfu  7554  mulnqprlemfl  7569  mulnqprlemfu  7570  recexprlemell  7616  recexprlemelu  7617  shftfvalg  10818  clim  11280  climmpt  11299  climshft2  11305  4sqlem2  12377  isstruct2r  12463  slotex  12479  setsvalg  12482  setsfun0  12488  setscom  12492  ressvalsets  12514  restval  12680  topnvalg  12686  plusffvalg  12711  grpidvalg  12722  sgrp1  12746  issubmnd  12773  issubm  12791  grppropstrg  12823  grpinvfvalg  12843  grpinvfng  12845  grpsubfvalg  12846  grpressid  12859  mulgfvalg  12913  mulgfng  12915  issubg  12960  mgpvalg  13033  mgptopng  13039  ringidvalg  13044  dfur2g  13045  issrg  13048  iscrng2  13098  opprvalg  13140  reldvdsrsrg  13160  dvdsrex  13166  unitgrp  13184  unitabl  13185  unitlinv  13194  unitrinv  13195  aprap  13243  toponsspwpwg  13302  tgval  13331  eltg  13334  eltg2  13335  restbasg  13450  tgrest  13451  txvalex  13536  txval  13537  ispsmet  13605  ismet  13626  isxmet  13627  xmetunirn  13640  blfvalps  13667  bj-vtoclgft  14298  djucllem  14323  bj-nvel  14420