Theorem ifr0

Description: A class that is founded by the identity relation is null. (Contributed by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	ifr0	$$⊢\mathrm{I}\mathrm{Fr}A\leftrightarrow A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		equid	$$⊢x=x$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	ideq	$$⊢x\mathrm{I}x\leftrightarrow x=x$$
4	1 3	mpbir	$$⊢x\mathrm{I}x$$
5		frirr	$$⊢\left(\mathrm{I}\mathrm{Fr}A\wedge x\in A\right)\to \neg x\mathrm{I}x$$
6	5	ex	$$⊢\mathrm{I}\mathrm{Fr}A\to \left(x\in A\to \neg x\mathrm{I}x\right)$$
7	4 6	mt2i	$$⊢\mathrm{I}\mathrm{Fr}A\to \neg x\in A$$
8	7	eq0rdv	$$⊢\mathrm{I}\mathrm{Fr}A\to A=\varnothing$$
9		fr0	$$⊢\mathrm{I}\mathrm{Fr}\varnothing$$
10		freq2	$$⊢A=\varnothing \to \left(\mathrm{I}\mathrm{Fr}A\leftrightarrow \mathrm{I}\mathrm{Fr}\varnothing \right)$$
11	9 10	mpbiri	$$⊢A=\varnothing \to \mathrm{I}\mathrm{Fr}A$$
12	8 11	impbii	$$⊢\mathrm{I}\mathrm{Fr}A\leftrightarrow A=\varnothing$$