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

Metamath Proof Explorer

Theorem dfepfr

Description: An alternate way of saying that the membership relation is well-founded. (Contributed by NM, 17-Feb-2004) (Revised by Mario Carneiro, 23-Jun-2015)

		Ref	Expression
	Assertion	dfepfr	$⊢ E Fr A \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap y = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		dffr2	$⊢ E Fr A \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \{z \in x \| z E y\} = \emptyset)$
2		epel	$⊢ z E y \leftrightarrow z \in y$
3	2	rabbii	$⊢ \{z \in x \| z E y\} = \{z \in x \| z \in y\}$
4		dfin5	$⊢ x \cap y = \{z \in x \| z \in y\}$
5	3 4	eqtr4i	$⊢ \{z \in x \| z E y\} = x \cap y$
6	5	eqeq1i	$⊢ \{z \in x \| z E y\} = \emptyset \leftrightarrow x \cap y = \emptyset$
7	6	rexbii	$⊢ \exists y \in x \{z \in x \| z E y\} = \emptyset \leftrightarrow \exists y \in x x \cap y = \emptyset$
8	7	imbi2i	$⊢ ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \{z \in x \| z E y\} = \emptyset) \leftrightarrow ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap y = \emptyset)$
9	8	albii	$⊢ \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \{z \in x \| z E y\} = \emptyset) \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap y = \emptyset)$
10	1 9	bitri	$⊢ E Fr A \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap y = \emptyset)$