Theorem epfrc

Description: A subset of a well-founded class has a minimal element. (Contributed by NM, 17-Feb-2004) (Revised by David Abernethy, 22-Feb-2011)

	Ref	Expression
Hypothesis	epfrc.1	$$⊢B\in \mathrm{V}$$
Assertion	epfrc	$$⊢\left(\mathrm{E}\mathrm{Fr}A\wedge B\subseteq A\wedge B\ne \varnothing \right)\to \exists x\in BB\cap x=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		epfrc.1	$$⊢B\in \mathrm{V}$$
2	1	frc	$$⊢\left(\mathrm{E}\mathrm{Fr}A\wedge B\subseteq A\wedge B\ne \varnothing \right)\to \exists x\in B\left\{y\in B|y\mathrm{E}x\right\}=\varnothing$$
3		dfin5	$$⊢B\cap x=\left\{y\in B|y\in x\right\}$$
4		epel	$$⊢y\mathrm{E}x\leftrightarrow y\in x$$
5	4	rabbii	$$⊢\left\{y\in B|y\mathrm{E}x\right\}=\left\{y\in B|y\in x\right\}$$
6	3 5	eqtr4i	$$⊢B\cap x=\left\{y\in B|y\mathrm{E}x\right\}$$
7	6	eqeq1i	$$⊢B\cap x=\varnothing \leftrightarrow \left\{y\in B|y\mathrm{E}x\right\}=\varnothing$$
8	7	rexbii	$$⊢\exists x\in BB\cap x=\varnothing \leftrightarrow \exists x\in B\left\{y\in B|y\mathrm{E}x\right\}=\varnothing$$
9	2 8	sylibr	$$⊢\left(\mathrm{E}\mathrm{Fr}A\wedge B\subseteq A\wedge B\ne \varnothing \right)\to \exists x\in BB\cap x=\varnothing$$