Theorem zfregfr

Description: The membership relation is well-founded on any class. (Contributed by NM, 26-Nov-1995)

	Ref	Expression
Assertion	zfregfr	$$⊢\mathrm{E}\mathrm{Fr}A$$

Proof

Step	Hyp	Ref	Expression
1		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)$$
2		vex	$$⊢x\in \mathrm{V}$$
3		zfreg	$$⊢\left(x\in \mathrm{V}\wedge x\ne \varnothing \right)\to \exists y\in xy\cap x=\varnothing$$
4	2 3	mpan	$$⊢x\ne \varnothing \to \exists y\in xy\cap x=\varnothing$$
5		incom	$$⊢y\cap x=x\cap y$$
6	5	eqeq1i	$$⊢y\cap x=\varnothing \leftrightarrow x\cap y=\varnothing$$
7	6	rexbii	$$⊢\exists y\in xy\cap x=\varnothing \leftrightarrow \exists y\in xx\cap y=\varnothing$$
8	4 7	sylib	$$⊢x\ne \varnothing \to \exists y\in xx\cap y=\varnothing$$
9	8	adantl	$$⊢\left(x\subseteq A\wedge x\ne \varnothing \right)\to \exists y\in xx\cap y=\varnothing$$
10	1 9	mpgbir	$$⊢\mathrm{E}\mathrm{Fr}A$$