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	$$⊢\psi$$
Assertion	bj-rababw	$$⊢\left\{x\in \left\{y|\psi \right\}|\phi \right\}=\left\{x|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		bj-rababw.1	$$⊢\psi$$
2		df-rab	$$⊢\left\{x\in \left\{y|\psi \right\}|\phi \right\}=\left\{x|\left(x\in \left\{y|\psi \right\}\wedge \phi \right)\right\}$$
3	1	vexw	$$⊢x\in \left\{y|\psi \right\}$$
4	3	biantrur	$$⊢\phi \leftrightarrow \left(x\in \left\{y|\psi \right\}\wedge \phi \right)$$
5	4	abbii	$$⊢\left\{x|\phi \right\}=\left\{x|\left(x\in \left\{y|\psi \right\}\wedge \phi \right)\right\}$$
6	2 5	eqtr4i	$$⊢\left\{x\in \left\{y|\psi \right\}|\phi \right\}=\left\{x|\phi \right\}$$