Theorem intex 5314

Description: The intersection of a nonempty class exists. Exercise 5 of [TakeutiZaring] p. 44 and its converse. (Contributed by NM, 13-Aug-2002.)

Assertion

Ref	Expression
intex	⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Proof of Theorem intex

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		n0 4328	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4939	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3463	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5291	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1930	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 217	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5285	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4925	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4938	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2786	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2819	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 327	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2961	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 209	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2108   ≠ wne 2932  Vcvv 3459   ⊆ wss 3926  ∅c0 4308  ∩ cint 4922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-in 3933  df-ss 3943  df-nul 4309  df-int 4923

This theorem is referenced by:  intnex  5315  intexab  5316  iinexg  5318  onint0  7785  onintrab  7790  onmindif2  7801  fival  9424  elfi2  9426  elfir  9427  dffi2  9435  elfiun  9442  fifo  9444  tz9.1c  9744  tz9.12lem1  9801  tz9.12lem3  9803  rankf  9808  cardf2  9957  cardval3  9966  cardid2  9967  cardcf  10266  cflim2  10277  intwun  10749  wuncval  10756  inttsk  10788  intgru  10828  gruina  10832  dfrtrcl2  15081  mremre  17616  mrcval  17622  asplss  21834  aspsubrg  21836  toponmre  23031  subbascn  23192  zarclsint  33903  insiga  34168  sigagenval  34171  sigagensiga  34172  dmsigagen  34175  dfon2lem8  35808  dfon2lem9  35809  bj-snmoore  37131  igenval  38085  pclvalN  39909  elrfi  42717  ismrcd1  42721  mzpval  42755  dmmzp  42756  oninfex2  43269  salgenval  46350  intsal  46359