Theorem bj-rabtr

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

	Ref	Expression
Assertion	bj-rabtr	$$⊢\left\{x\in A|\top \right\}=A$$

Proof

Step	Hyp	Ref	Expression
1		ssrab2	$$⊢\left\{x\in A|\top \right\}\subseteq A$$
2		ssid	$$⊢A\subseteq A$$
3		tru	$$⊢\top$$
4	3	rgenw	$$⊢\forall x\in A\top$$
5		ssrab	$$⊢A\subseteq \left\{x\in A|\top \right\}\leftrightarrow \left(A\subseteq A\wedge \forall x\in A\top \right)$$
6	2 4 5	mpbir2an	$$⊢A\subseteq \left\{x\in A|\top \right\}$$
7	1 6	eqssi	$$⊢\left\{x\in A|\top \right\}=A$$