Theorem bj-rababw

Description: A weak version of rabab not using df-clel nor df-v (but requiring ax-ext ) nor ax-12 . (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	bj-rababw.1	|- ps
Assertion	bj-rababw	|- { x e. { y | ps } | ph } = { x | ph }

Proof

Step	Hyp	Ref	Expression
1		bj-rababw.1	|- ps
2		df-rab	|- { x e. { y | ps } | ph } = { x | ( x e. { y | ps } /\ ph ) }
3	1	vexw	|- x e. { y | ps }
4	3	biantrur	|- ( ph <-> ( x e. { y | ps } /\ ph ) )
5	4	abbii	|- { x | ph } = { x | ( x e. { y | ps } /\ ph ) }
6	2 5	eqtr4i	|- { x e. { y | ps } | ph } = { x | ph }