Theorem sseli 3270

Description: Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
sseli.1	|- A C_ B

Assertion

Ref	Expression
sseli	|- (C e. A -> C e. B)

Proof of Theorem sseli

Step	Hyp	Ref	Expression
1		sseli.1	. 2 |- A C_ B
2		ssel 3268	. 2 |- (A C_ B -> (C e. A -> C e. B))
3	1, 2	ax-mp 5	1 |- (C e. A -> C e. B)

Syntax hints:   -> wi 4   e. wcel 1710   C_ wss 3258

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-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-ss 3260

This theorem is referenced by:  sselii  3271  sseldi  3272  elun1  3431  elun2  3432  opkelimagekg  4272  cokrelk  4285  eqpw1uni  4331  dfnnc2  4396  peano5  4410  nnsucelr  4429  vfinspss  4552  phi011lem1  4599  phialllem2  4618  2elresin  5195  fvopab4ndm  5391  fvimacnvi  5403  elpreima  5408  fvmptss  5706  fvmptex  5722  fvmptnf  5724  clos1is  5882  clos1basesuc  5883  erdisj  5973  enadjlem1  6060