Theorem intex 5344

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 4353	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4963	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3484	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5321	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1930	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 217	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5315	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4949	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4962	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2793	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2826	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 327	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2970	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 209	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2108   ≠ wne 2940  Vcvv 3480   ⊆ wss 3951  ∅c0 4333  ∩ cint 4946

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 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-in 3958  df-ss 3968  df-nul 4334  df-int 4947

This theorem is referenced by:  intnex  5345  intexab  5346  iinexg  5348  onint0  7811  onintrab  7816  onmindif2  7827  fival  9452  elfi2  9454  elfir  9455  dffi2  9463  elfiun  9470  fifo  9472  tz9.1c  9770  tz9.12lem1  9827  tz9.12lem3  9829  rankf  9834  cardf2  9983  cardval3  9992  cardid2  9993  cardcf  10292  cflim2  10303  intwun  10775  wuncval  10782  inttsk  10814  intgru  10854  gruina  10858  dfrtrcl2  15101  mremre  17647  mrcval  17653  asplss  21894  aspsubrg  21896  toponmre  23101  subbascn  23262  zarclsint  33871  insiga  34138  sigagenval  34141  sigagensiga  34142  dmsigagen  34145  dfon2lem8  35791  dfon2lem9  35792  bj-snmoore  37114  igenval  38068  pclvalN  39892  elrfi  42705  ismrcd1  42709  mzpval  42743  dmmzp  42744  oninfex2  43257  salgenval  46336  intsal  46345