exse2

Description: Any set relation is set-like. (Contributed by Mario Carneiro, 22-Jun-2015)

		Ref	Expression
	Assertion	exse2	$⊢ R \in V \to R Se A$

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{y \in A \| y R x\} = \{y \| (y \in A \land y R x)\}$
2		vex	$⊢ y \in V$
3		vex	$⊢ x \in V$
4	2 3	breldm	$⊢ y R x \to y \in dom R$
5	4	adantl	$⊢ (y \in A \land y R x) \to y \in dom R$
6	5	abssi	$⊢ \{y \| (y \in A \land y R x)\} \subseteq dom R$
7	1 6	eqsstri	$⊢ \{y \in A \| y R x\} \subseteq dom R$
8		dmexg	$⊢ R \in V \to dom R \in V$
9		ssexg	$⊢ (\{y \in A \| y R x\} \subseteq dom R \land dom R \in V) \to \{y \in A \| y R x\} \in V$
10	7 8 9	sylancr	$⊢ R \in V \to \{y \in A \| y R x\} \in V$
11	10	ralrimivw	$⊢ R \in V \to \forall x \in A \{y \in A \| y R x\} \in V$
12		df-se	$⊢ R Se A \leftrightarrow \forall x \in A \{y \in A \| y R x\} \in V$
13	11 12	sylibr	$⊢ R \in V \to R Se A$

Metamath Proof Explorer