bj-rabtr

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

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

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

Metamath Proof Explorer