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	|- { x e. A | T. } = A

Proof

Step	Hyp	Ref	Expression
1		ssrab2	|- { x e. A | T. } C_ A
2		ssid	|- A C_ A
3	2	a1i	|- ( T. -> A C_ A )
4		simpl	|- ( ( T. /\ x e. A ) -> T. )
5	3 4	ssrabdv	|- ( T. -> A C_ { x e. A | T. } )
6	5	mptru	|- A C_ { x e. A | T. }
7	1 6	eqssi	|- { x e. A | T. } = A