Theorem bj-rabtrAUTO

Description: Proof of bj-rabtr found automatically by the Metamath program "MM-PA> IMPROVE ALL / DEPTH 3 / 3" command followed by "MM-PA> MINIMIZE__WITH *". (Contributed by BJ, 22-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-rabtrAUTO	$$⊢\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	2	a1i	$$⊢\top \to A\subseteq A$$
4		simpl	$$⊢\left(\top \wedge x\in A\right)\to \top$$
5	3 4	ssrabdv	$$⊢\top \to A\subseteq \left\{x\in A|\top \right\}$$
6	5	mptru	$$⊢A\subseteq \left\{x\in A|\top \right\}$$
7	1 6	eqssi	$$⊢\left\{x\in A|\top \right\}=A$$