Theorem intnex

Description: If a class intersection is not a set, it must be the universe. (Contributed by NM, 3-Jul-2005)

	Ref	Expression
Assertion	intnex	⊢ ( ¬ ∩ 𝐴 ∈ V ↔ ∩ 𝐴 = V )

Proof

Step	Hyp	Ref	Expression
1		intex	⊢ ( 𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V )
2	1	necon1bbii	⊢ ( ¬ ∩ 𝐴 ∈ V ↔ 𝐴 = ∅ )
3		inteq	⊢ ( 𝐴 = ∅ → ∩ 𝐴 = ∩ ∅ )
4		int0	⊢ ∩ ∅ = V
5	3 4	eqtrdi	⊢ ( 𝐴 = ∅ → ∩ 𝐴 = V )
6	2 5	sylbi	⊢ ( ¬ ∩ 𝐴 ∈ V → ∩ 𝐴 = V )
7		vprc	⊢ ¬ V ∈ V
8		eleq1	⊢ ( ∩ 𝐴 = V → ( ∩ 𝐴 ∈ V ↔ V ∈ V ) )
9	7 8	mtbiri	⊢ ( ∩ 𝐴 = V → ¬ ∩ 𝐴 ∈ V )
10	6 9	impbii	⊢ ( ¬ ∩ 𝐴 ∈ V ↔ ∩ 𝐴 = V )