Theorem dfse2

Description: Alternate definition of set-like relation. (Contributed by Mario Carneiro, 23-Jun-2015)

	Ref	Expression
Assertion	dfse2	$$⊢R\mathrm{Se}A\leftrightarrow \forall x\in AA\cap R^{-1}\left[\left\{x\right\}\right]\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-se	$$⊢R\mathrm{Se}A\leftrightarrow \forall x\in A\left\{y\in A|yRx\right\}\in \mathrm{V}$$
2		dfrab3	$$⊢\left\{y\in A|yRx\right\}=A\cap \left\{y|yRx\right\}$$
3		iniseg	$$⊢x\in \mathrm{V}\to R^{-1}\left[\left\{x\right\}\right]=\left\{y|yRx\right\}$$
4	3	elv	$$⊢R^{-1}\left[\left\{x\right\}\right]=\left\{y|yRx\right\}$$
5	4	ineq2i	$$⊢A\cap R^{-1}\left[\left\{x\right\}\right]=A\cap \left\{y|yRx\right\}$$
6	2 5	eqtr4i	$$⊢\left\{y\in A|yRx\right\}=A\cap R^{-1}\left[\left\{x\right\}\right]$$
7	6	eleq1i	$$⊢\left\{y\in A|yRx\right\}\in \mathrm{V}\leftrightarrow A\cap R^{-1}\left[\left\{x\right\}\right]\in \mathrm{V}$$
8	7	ralbii	$$⊢\forall x\in A\left\{y\in A|yRx\right\}\in \mathrm{V}\leftrightarrow \forall x\in AA\cap R^{-1}\left[\left\{x\right\}\right]\in \mathrm{V}$$
9	1 8	bitri	$$⊢R\mathrm{Se}A\leftrightarrow \forall x\in AA\cap R^{-1}\left[\left\{x\right\}\right]\in \mathrm{V}$$