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

Metamath Proof Explorer

Theorem eqabdv

Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994) Avoid ax-11 . (Revised by Wolf Lammen, 6-May-2023)

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

Step	Hyp	Ref	Expression
1		eqabdv.1	$⊢ φ \to (x \in A \leftrightarrow ψ)$
2	1	sbbidv	$⊢ φ \to ([y/ x] x \in A \leftrightarrow [y/ x] ψ)$
3		clelsb1	$⊢ [y/ x] x \in A \leftrightarrow y \in A$
4	3	bicomi	$⊢ y \in A \leftrightarrow [y/ x] x \in A$
5		df-clab	$⊢ y \in \{x \| ψ\} \leftrightarrow [y/ x] ψ$
6	2 4 5	3bitr4g	$⊢ φ \to (y \in A \leftrightarrow y \in \{x \| ψ\})$
7	6	eqrdv	$⊢ φ \to A = \{x \| ψ\}$