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	|- ( Rel |^| { x | ph } -> E. x ph )

Proof

Step	Hyp	Ref	Expression
1		intnex	|- ( -. |^| { x | ph } e. _V <-> |^| { x | ph } = _V )
2		nrelv	|- -. Rel _V
3		releq	|- ( |^| { x | ph } = _V -> ( Rel |^| { x | ph } <-> Rel _V ) )
4	2 3	mtbiri	|- ( |^| { x | ph } = _V -> -. Rel |^| { x | ph } )
5	1 4	sylbi	|- ( -. |^| { x | ph } e. _V -> -. Rel |^| { x | ph } )
6	5	con4i	|- ( Rel |^| { x | ph } -> |^| { x | ph } e. _V )
7		intexab	|- ( E. x ph <-> |^| { x | ph } e. _V )
8	6 7	sylibr	|- ( Rel |^| { x | ph } -> E. x ph )