Theorem elex 2868

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 ∈ B → A ∈ V)

Proof of Theorem elex

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		exsimpl 1592	. 2 ⊢ (∃x(x = A ∧ x ∈ B) → ∃x x = A)
2		df-clel 2349	. 2 ⊢ (A ∈ B ↔ ∃x(x = A ∧ x ∈ B))
3		isset 2864	. 2 ⊢ (A ∈ V ↔ ∃x x = A)
4	1, 2, 3	3imtr4i 257	1 ⊢ (A ∈ B → A ∈ V)

Syntax hints:   → wi 4   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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 2862

This theorem is referenced by:  elexi  2869  elisset  2870  vtoclgft  2906  vtoclgf  2914  vtocl2gf  2917  vtocl3gf  2918  spcimgft  2931  elab4g  2990  elrabf  2994  mob  3019  sbcex  3056  sbcieg  3079  sbcrext  3120  sbcabel  3124  csbexg  3147  csbcomg  3160  csbvarg  3164  csbiebt  3173  csbnestgf  3185  csbidmg  3191  sbcco3g  3192  csbco3g  3194  elin  3220  elun  3221  ssv  3292  snidb  3760  ifpr  3775  eluni  3895  eliun  3974  el1c  4140  elxpk  4197  opkelopkabg  4246  opkelcokg  4262  opkelimagekg  4272  setswith  4322  euabex  4335  iota2  4368  eladdc  4399  ncfinlower  4484  opeqex  4622  brex  4690  elopab  4697  elima  4755  epelc  4766  opeliunxp  4821  eliunxp  4822  opeliunxp2  4823  ideqg  4869  ideqg2  4870  opeldm  4911  elimasn  5020  fvelimab  5371  fvopab4t  5386  fvopabg  5392  eloprabga  5579  dmmptg  5685  fnmpt  5690  ov2gf  5712  fvmptf  5723  fnmpt2  5733  elfix  5788  otelins2  5792  otelins3  5793  oqelins4  5795  cupvalg  5813  composevalg  5818  ovcross  5846  brfullfung  5866  fvdomfn  5869  fvranfn  5870  erref  5960  erth  5969  erth2  5970  mapvalg  6010  pmvalg  6011  elncs  6120  elnc  6126  eqncg  6127  elce  6176  ce0nnuli  6179  spacind  6288  elcan  6330  elscan  6331