Theorem intex 5339

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 4347	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4966	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3467	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5321	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1925	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 216	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5315	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4952	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4965	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2781	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2810	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 326	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2960	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 208	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 205   = wceq 1533  ∃wex 1773   ∈ wcel 2098   ≠ wne 2930  Vcvv 3463   ⊆ wss 3945  ∅c0 4323  ∩ cint 4949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5299

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3465  df-dif 3948  df-in 3952  df-ss 3962  df-nul 4324  df-int 4950

This theorem is referenced by:  intnex  5340  intexab  5341  iinexg  5343  onint0  7793  onintrab  7798  onmindif2  7809  fival  9435  elfi2  9437  elfir  9438  dffi2  9446  elfiun  9453  fifo  9455  tz9.1c  9753  tz9.12lem1  9810  tz9.12lem3  9812  rankf  9817  cardf2  9966  cardval3  9975  cardid2  9976  cardcf  10275  cflim2  10286  intwun  10758  wuncval  10765  inttsk  10797  intgru  10837  gruina  10841  dfrtrcl2  15041  mremre  17583  mrcval  17589  asplss  21811  aspsubrg  21813  toponmre  23027  subbascn  23188  zarclsint  33543  insiga  33826  sigagenval  33829  sigagensiga  33830  dmsigagen  33833  dfon2lem8  35456  dfon2lem9  35457  bj-snmoore  36662  igenval  37604  pclvalN  39432  elrfi  42179  ismrcd1  42183  mzpval  42217  dmmzp  42218  oninfex2  42738  salgenval  45772  intsal  45781