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	$$⊢\phi \to \psi$$
Assertion	ss2abi	$$⊢\left\{x|\phi \right\}\subseteq \left\{x|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		ss2abi.1	$$⊢\phi \to \psi$$
2		tru	$$⊢\top$$
3	1	a1i	$$⊢\top \to \left(\phi \to \psi \right)$$
4	3	ss2abdv	$$⊢\top \to \left\{x|\phi \right\}\subseteq \left\{x|\psi \right\}$$
5	2 4	ax-mp	$$⊢\left\{x|\phi \right\}\subseteq \left\{x|\psi \right\}$$