Theorem bj-reabeq

Description: Relative form of abeq2 . (Contributed by BJ, 27-Dec-2023)

	Ref	Expression
Assertion	bj-reabeq	$$⊢V\cap A=\left\{x\in V|\phi \right\}\leftrightarrow \forall x\in V\left(x\in A\leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		dfrab3	$$⊢\left\{x\in V|\phi \right\}=V\cap \left\{x|\phi \right\}$$
2	1	eqeq2i	$$⊢V\cap A=\left\{x\in V|\phi \right\}\leftrightarrow V\cap A=V\cap \left\{x|\phi \right\}$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
4		nfab1	$$⊢\underset{\_}{Ⅎ}x\left\{x|\phi \right\}$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xV$$
6	3 4 5	bj-rcleqf	$$⊢V\cap A=V\cap \left\{x|\phi \right\}\leftrightarrow \forall x\in V\left(x\in A\leftrightarrow x\in \left\{x|\phi \right\}\right)$$
7		abid	$$⊢x\in \left\{x|\phi \right\}\leftrightarrow \phi$$
8	7	bibi2i	$$⊢\left(x\in A\leftrightarrow x\in \left\{x|\phi \right\}\right)\leftrightarrow \left(x\in A\leftrightarrow \phi \right)$$
9	8	ralbii	$$⊢\forall x\in V\left(x\in A\leftrightarrow x\in \left\{x|\phi \right\}\right)\leftrightarrow \forall x\in V\left(x\in A\leftrightarrow \phi \right)$$
10	2 6 9	3bitri	$$⊢V\cap A=\left\{x\in V|\phi \right\}\leftrightarrow \forall x\in V\left(x\in A\leftrightarrow \phi \right)$$