Theorem bj-rabtr

Description: Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019)

	Ref	Expression
Assertion	bj-rabtr	|- { x e. A | T. } = A

Proof

Step	Hyp	Ref	Expression
1		ssrab2	|- { x e. A | T. } C_ A
2		ssid	|- A C_ A
3		tru	|- T.
4	3	rgenw	|- A. x e. A T.
5		ssrab	|- ( A C_ { x e. A | T. } <-> ( A C_ A /\ A. x e. A T. ) )
6	2 4 5	mpbir2an	|- A C_ { x e. A | T. }
7	1 6	eqssi	|- { x e. A | T. } = A