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 ∩ { 𝑥 ∣ 𝜑 } → ∃ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		intnex	⊢ ( ¬ ∩ { 𝑥 ∣ 𝜑 } ∈ V ↔ ∩ { 𝑥 ∣ 𝜑 } = V )
2		nrelv	⊢ ¬ Rel V
3		releq	⊢ ( ∩ { 𝑥 ∣ 𝜑 } = V → ( Rel ∩ { 𝑥 ∣ 𝜑 } ↔ Rel V ) )
4	2 3	mtbiri	⊢ ( ∩ { 𝑥 ∣ 𝜑 } = V → ¬ Rel ∩ { 𝑥 ∣ 𝜑 } )
5	1 4	sylbi	⊢ ( ¬ ∩ { 𝑥 ∣ 𝜑 } ∈ V → ¬ Rel ∩ { 𝑥 ∣ 𝜑 } )
6	5	con4i	⊢ ( Rel ∩ { 𝑥 ∣ 𝜑 } → ∩ { 𝑥 ∣ 𝜑 } ∈ V )
7		intexab	⊢ ( ∃ 𝑥 𝜑 ↔ ∩ { 𝑥 ∣ 𝜑 } ∈ V )
8	6 7	sylibr	⊢ ( Rel ∩ { 𝑥 ∣ 𝜑 } → ∃ 𝑥 𝜑 )