dfse2

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

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

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

Metamath Proof Explorer