Theorem intnex 5306

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

Assertion

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

Proof of Theorem intnex

Step	Hyp	Ref	Expression
1		intex 5305	. . . 4 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)
2	1	necon1bbii 3005	. . 3 ⊢ (¬ ∩ 𝐴 ∈ V ↔ 𝐴 = ∅)
3		inteq 4910	. . . 4 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
4		int0 4922	. . . 4 ⊢ ∩ ∅ = V
5	3, 4	eqtrdi 2812	. . 3 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
6	2, 5	sylbi 220	. 2 ⊢ (¬ ∩ 𝐴 ∈ V → ∩ 𝐴 = V)
7		vprc 5274	. . 3 ⊢ ¬ V ∈ V
8		eleq1 2849	. . 3 ⊢ (∩ 𝐴 = V → (∩ 𝐴 ∈ V ↔ V ∈ V))
9	7, 8	mtbiri 330	. 2 ⊢ (∩ 𝐴 = V → ¬ ∩ 𝐴 ∈ V)
10	6, 9	impbii 212	1 ⊢ (¬ ∩ 𝐴 ∈ V ↔ ∩ 𝐴 = V)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1570   ∈ wcel 2145  Vcvv 3451  ∅c0 4279  ∩ cint 4907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-in 3906  df-ss 3916  df-nul 4280  df-int 4908

This theorem is used by:  intabs  5310  relintabex  44566  aiotavb  48129