Theorem relintabex

Description: If the intersection of a class is a relation, then the class is nonempty. (Contributed by RP, 12-Aug-2020)

	Ref	Expression
Assertion	relintabex	$$⊢\mathrm{Rel}\bigcap \left\{x|\phi \right\}\to \exists x\phi$$

Proof

Step	Hyp	Ref	Expression
1		intnex	$$⊢\neg \bigcap \left\{x|\phi \right\}\in \mathrm{V}\leftrightarrow \bigcap \left\{x|\phi \right\}=\mathrm{V}$$
2		nrelv	$$⊢\neg \mathrm{Rel}\mathrm{V}$$
3		releq	$$⊢\bigcap \left\{x|\phi \right\}=\mathrm{V}\to \left(\mathrm{Rel}\bigcap \left\{x|\phi \right\}\leftrightarrow \mathrm{Rel}\mathrm{V}\right)$$
4	2 3	mtbiri	$$⊢\bigcap \left\{x|\phi \right\}=\mathrm{V}\to \neg \mathrm{Rel}\bigcap \left\{x|\phi \right\}$$
5	1 4	sylbi	$$⊢\neg \bigcap \left\{x|\phi \right\}\in \mathrm{V}\to \neg \mathrm{Rel}\bigcap \left\{x|\phi \right\}$$
6	5	con4i	$$⊢\mathrm{Rel}\bigcap \left\{x|\phi \right\}\to \bigcap \left\{x|\phi \right\}\in \mathrm{V}$$
7		intexab	$$⊢\exists x\phi \leftrightarrow \bigcap \left\{x|\phi \right\}\in \mathrm{V}$$
8	6 7	sylibr	$$⊢\mathrm{Rel}\bigcap \left\{x|\phi \right\}\to \exists x\phi$$