This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfse3

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

		Ref	Expression
	Assertion	dfse3	$⊢ R Se A \leftrightarrow \forall x \in A Pred (R, A, x) \in V$

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