Theorem eqrrabd

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

	Ref	Expression
Hypotheses	eqrrabd.1	$$⊢\phi \to B\subseteq A$$
	eqrrabd.2	$$⊢\left(\phi \wedge x\in A\right)\to \left(x\in B\leftrightarrow \psi \right)$$
Assertion	eqrrabd	$$⊢\phi \to B=\left\{x\in A|\psi \right\}$$

Proof

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