eqrrabd

Description: Deduce equality with a restricted abstraction. (Contributed by Thierry Arnoux, 11-Apr-2024)

	Ref	Expression
Hypotheses	eqrrabd.1	$⊢ φ \to B \subseteq A$
	eqrrabd.2	$⊢ (φ \land x \in A) \to (x \in B \leftrightarrow ψ)$
Assertion	eqrrabd	$⊢ φ \to B = \{x \in A \| ψ\}$

Step	Hyp	Ref	Expression
1		eqrrabd.1	$⊢ φ \to B \subseteq A$
2		eqrrabd.2	$⊢ (φ \land x \in A) \to (x \in B \leftrightarrow ψ)$
3		nfv	$⊢ Ⅎ x φ$
4		nfcv	$⊢ \underline{Ⅎ} x B$
5		nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| ψ\}$
6	1	sseld	$⊢ φ \to (x \in B \to x \in A)$
7	6	pm4.71rd	$⊢ φ \to (x \in B \leftrightarrow (x \in A \land x \in B))$
8	2	pm5.32da	$⊢ φ \to ((x \in A \land x \in B) \leftrightarrow (x \in A \land ψ))$
9	7 8	bitrd	$⊢ φ \to (x \in B \leftrightarrow (x \in A \land ψ))$
10		rabid	$⊢ x \in \{x \in A \| ψ\} \leftrightarrow (x \in A \land ψ)$
11	9 10	bitr4di	$⊢ φ \to (x \in B \leftrightarrow x \in \{x \in A \| ψ\})$
12	3 4 5 11	eqrd	$⊢ φ \to B = \{x \in A \| ψ\}$

Metamath Proof Explorer