Theorem eqrrabd

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

	Ref	Expression
Hypotheses	eqrrabd.1	|- ( ph -> B C_ A )
	eqrrabd.2	|- ( ( ph /\ x e. A ) -> ( x e. B <-> ps ) )
Assertion	eqrrabd	|- ( ph -> B = { x e. A | ps } )

Proof

Step	Hyp	Ref	Expression
1		eqrrabd.1	|- ( ph -> B C_ A )
2		eqrrabd.2	|- ( ( ph /\ x e. A ) -> ( x e. B <-> ps ) )
3		nfv	|- F/ x ph
4		nfcv	|- F/_ x B
5		nfrab1	|- F/_ x { x e. A | ps }
6	1	sseld	|- ( ph -> ( x e. B -> x e. A ) )
7	6	pm4.71rd	|- ( ph -> ( x e. B <-> ( x e. A /\ x e. B ) ) )
8	2	pm5.32da	|- ( ph -> ( ( x e. A /\ x e. B ) <-> ( x e. A /\ ps ) ) )
9	7 8	bitrd	|- ( ph -> ( x e. B <-> ( x e. A /\ ps ) ) )
10		rabid	|- ( x e. { x e. A | ps } <-> ( x e. A /\ ps ) )
11	9 10	bitr4di	|- ( ph -> ( x e. B <-> x e. { x e. A | ps } ) )
12	3 4 5 11	eqrd	|- ( ph -> B = { x e. A | ps } )