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

Metamath Proof Explorer

Theorem eqabcdv

Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994) (Proof shortened by Wolf Lammen, 16-Nov-2019)

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

Step	Hyp	Ref	Expression
1		eqabcdv.1	$⊢ φ \to (ψ \leftrightarrow x \in A)$
2	1	bicomd	$⊢ φ \to (x \in A \leftrightarrow ψ)$
3	2	eqabdv	$⊢ φ \to A = \{x \| ψ\}$
4	3	eqcomd	$⊢ φ \to \{x \| ψ\} = A$