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

Metamath Proof Explorer

Theorem ssabdv

Description: Deduction of abstraction subclass from implication. (Contributed by SN, 22-Dec-2024)

		Ref	Expression
	Hypothesis	ssabdv.1	$⊢ φ \to (x \in A \to ψ)$
	Assertion	ssabdv	$⊢ φ \to A \subseteq \{x \| ψ\}$

Step	Hyp	Ref	Expression
1		ssabdv.1	$⊢ φ \to (x \in A \to ψ)$
2		abid1	$⊢ A = \{x \| x \in A\}$
3	1	ss2abdv	$⊢ φ \to \{x \| x \in A\} \subseteq \{x \| ψ\}$
4	2 3	eqsstrid	$⊢ φ \to A \subseteq \{x \| ψ\}$