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	$$⊢\mathrm{E}\mathrm{Fr}A\leftrightarrow \forall x\left(\left(x\subseteq A\wedge x\ne \varnothing \right)\to \exists y\in xx\cap y=\varnothing \right)$$

Proof

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