Theorem elex 2867

Description: If a class is a member of another class, 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	|- (A e. B -> A e. _V)

Proof of Theorem elex

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		exsimpl 1592	. 2 |- (E.x(x = A /\ x e. B) -> E.x x = A)
2		df-clel 2349	. 2 |- (A e. B <-> E.x(x = A /\ x e. B))
3		isset 2863	. 2 |- (A e. _V <-> E.x x = A)
4	1, 2, 3	3imtr4i 257	1 |- (A e. B -> A e. _V)

Syntax hints:   -> wi 4   /\ wa 358  E.wex 1541   = wceq 1642   e. wcel 1710  _Vcvv 2859

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2861

This theorem is referenced by:  elexi  2868  elisset  2869  vtoclgft  2905  vtoclgf  2913  vtocl2gf  2916  vtocl3gf  2917  spcimgft  2930  elab4g  2989  elrabf  2993  mob  3018  sbcex  3055  sbcieg  3078  sbcrext  3119  sbcabel  3123  csbexg  3146  csbcomg  3159  csbvarg  3163  csbiebt  3172  csbnestgf  3184  csbidmg  3190  sbcco3g  3191  csbco3g  3193  elin  3219  elun  3220  ssv  3291  snidb  3759  ifpr  3774  eluni  3894  eliun  3973  el1c  4139  elxpk  4196  opkelopkabg  4245  opkelcokg  4261  opkelimagekg  4271  setswith  4321  euabex  4334  iota2  4367  eladdc  4398  ncfinlower  4483  opeqex  4621  brex  4689  elopab  4696  elima  4754  epelc  4765  opeliunxp  4820  eliunxp  4821  opeliunxp2  4822  ideqg  4868  ideqg2  4869  opeldm  4910  elimasn  5019  fvelimab  5370  fvopab4t  5385  fvopabg  5391  eloprabga  5578  dmmptg  5684  fnmpt  5689  ov2gf  5711  fvmptf  5722  fnmpt2  5732  elfix  5787  otelins2  5791  otelins3  5792  oqelins4  5794  cupvalg  5812  composevalg  5817  ovcross  5845  brfullfung  5865  fvdomfn  5868  fvranfn  5869  erref  5959  erth  5968  erth2  5969  mapvalg  6009  pmvalg  6010  elncs  6119  elnc  6125  eqncg  6126  elce  6175  ce0nnuli  6178  spacind  6287  elcan  6329  elscan  6330