# Metamath Proof Explorer

## 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}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 intnex ${⊢}¬\bigcap \left\{{x}|{\phi }\right\}\in \mathrm{V}↔\bigcap \left\{{x}|{\phi }\right\}=\mathrm{V}$
2 nrelv ${⊢}¬\mathrm{Rel}\mathrm{V}$
3 releq ${⊢}\bigcap \left\{{x}|{\phi }\right\}=\mathrm{V}\to \left(\mathrm{Rel}\bigcap \left\{{x}|{\phi }\right\}↔\mathrm{Rel}\mathrm{V}\right)$
4 2 3 mtbiri ${⊢}\bigcap \left\{{x}|{\phi }\right\}=\mathrm{V}\to ¬\mathrm{Rel}\bigcap \left\{{x}|{\phi }\right\}$
5 1 4 sylbi ${⊢}¬\bigcap \left\{{x}|{\phi }\right\}\in \mathrm{V}\to ¬\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}\phantom{\rule{.4em}{0ex}}{\phi }↔\bigcap \left\{{x}|{\phi }\right\}\in \mathrm{V}$
8 6 7 sylibr ${⊢}\mathrm{Rel}\bigcap \left\{{x}|{\phi }\right\}\to \exists {x}\phantom{\rule{.4em}{0ex}}{\phi }$