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

Metamath Proof Explorer

Theorem abssdv

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006) (Proof shortened by SN, 22-Dec-2024)

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

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