Theorem dfse3

Description: Alternate definition of set-like relationships. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Assertion	dfse3	$$⊢R\mathrm{Se}A\leftrightarrow \forall x\in APred\left(R,A,x\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		dfse2	$$⊢R\mathrm{Se}A\leftrightarrow \forall x\in AA\cap R^{-1}\left[\left\{x\right\}\right]\in \mathrm{V}$$
2		df-pred	$$⊢Pred\left(R,A,x\right)=A\cap R^{-1}\left[\left\{x\right\}\right]$$
3	2	eleq1i	$$⊢Pred\left(R,A,x\right)\in \mathrm{V}\leftrightarrow A\cap R^{-1}\left[\left\{x\right\}\right]\in \mathrm{V}$$
4	3	ralbii	$$⊢\forall x\in APred\left(R,A,x\right)\in \mathrm{V}\leftrightarrow \forall x\in AA\cap R^{-1}\left[\left\{x\right\}\right]\in \mathrm{V}$$
5	1 4	bitr4i	$$⊢R\mathrm{Se}A\leftrightarrow \forall x\in APred\left(R,A,x\right)\in \mathrm{V}$$