Theorem ss2abi

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995) Avoid ax-8 , ax-10 , ax-11 , ax-12 . (Revised by Gino Giotto, 28-Jun-2024)

	Ref	Expression
Hypothesis	ss2abi.1	|- ( ph -> ps )
Assertion	ss2abi	|- { x | ph } C_ { x | ps }

Proof

Step	Hyp	Ref	Expression
1		ss2abi.1	|- ( ph -> ps )
2		tru	|- T.
3	1	a1i	|- ( T. -> ( ph -> ps ) )
4	3	ss2abdv	|- ( T. -> { x | ph } C_ { x | ps } )
5	2 4	ax-mp	|- { x | ph } C_ { x | ps }