Theorem bj-rabtr

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

	Ref	Expression
Assertion	bj-rabtr	⊢ { 𝑥 ∈ 𝐴 ∣ ⊤ } = 𝐴

Proof

Step	Hyp	Ref	Expression
1		ssrab2	⊢ { 𝑥 ∈ 𝐴 ∣ ⊤ } ⊆ 𝐴
2		ssid	⊢ 𝐴 ⊆ 𝐴
3		tru	⊢ ⊤
4	3	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 ⊤
5		ssrab	⊢ ( 𝐴 ⊆ { 𝑥 ∈ 𝐴 ∣ ⊤ } ↔ ( 𝐴 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ⊤ ) )
6	2 4 5	mpbir2an	⊢ 𝐴 ⊆ { 𝑥 ∈ 𝐴 ∣ ⊤ }
7	1 6	eqssi	⊢ { 𝑥 ∈ 𝐴 ∣ ⊤ } = 𝐴