Theorem abssi

Description: Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006)

	Ref	Expression
Hypothesis	abssi.1	|- ( ph -> x e. A )
Assertion	abssi	|- { x | ph } C_ A

Proof

Step	Hyp	Ref	Expression
1		abssi.1	|- ( ph -> x e. A )
2	1	ss2abi	|- { x | ph } C_ { x | x e. A }
3		abid2	|- { x | x e. A } = A
4	2 3	sseqtri	|- { x | ph } C_ A