Theorem bj-inrab2

Description: Shorter proof of inrab . (Contributed by BJ, 21-Apr-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-inrab2	|- ( { x e. A | ph } i^i { x e. A | ps } ) = { x e. A | ( ph /\ ps ) }

Proof

Step	Hyp	Ref	Expression
1		bj-inrab	|- ( { x e. A | ph } i^i { x e. A | ps } ) = { x e. ( A i^i A ) | ( ph /\ ps ) }
2		nfv	|- F/ x T.
3		inidm	|- ( A i^i A ) = A
4	3	a1i	|- ( T. -> ( A i^i A ) = A )
5	2 4	bj-rabeqd	|- ( T. -> { x e. ( A i^i A ) | ( ph /\ ps ) } = { x e. A | ( ph /\ ps ) } )
6	5	mptru	|- { x e. ( A i^i A ) | ( ph /\ ps ) } = { x e. A | ( ph /\ ps ) }
7	1 6	eqtri	|- ( { x e. A | ph } i^i { x e. A | ps } ) = { x e. A | ( ph /\ ps ) }