This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 GG, 28-Jun-2024)

		Ref	Expression
	Hypothesis	ss2abi.1	$⊢ φ \to ψ$
	Assertion	ss2abi	$⊢ \{x \| φ\} \subseteq \{x \| ψ\}$

Proof

Step	Hyp	Ref	Expression
1		ss2abi.1	$⊢ φ \to ψ$
2		tru	$⊢ ⊤$
3	1	a1i	$⊢ ⊤ \to (φ \to ψ)$
4	3	ss2abdv	$⊢ ⊤ \to \{x \| φ\} \subseteq \{x \| ψ\}$
5	2 4	ax-mp	$⊢ \{x \| φ\} \subseteq \{x \| ψ\}$