Theorem intex 5281

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 4293	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4911	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3445	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5265	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1932	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 216	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5259	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4897	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4910	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2792	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2821	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 326	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2970	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 208	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 205   = wceq 1540  ∃wex 1780   ∈ wcel 2105   ≠ wne 2940  Vcvv 3441   ⊆ wss 3898  ∅c0 4269  ∩ cint 4894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-sep 5243

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2941  df-ral 3062  df-rab 3404  df-v 3443  df-dif 3901  df-in 3905  df-ss 3915  df-nul 4270  df-int 4895

This theorem is referenced by:  intnex  5282  intexab  5283  iinexg  5285  onint0  7704  onintrab  7709  onmindif2  7720  fival  9269  elfi2  9271  elfir  9272  dffi2  9280  elfiun  9287  fifo  9289  tz9.1c  9587  tz9.12lem1  9644  tz9.12lem3  9646  rankf  9651  cardf2  9800  cardval3  9809  cardid2  9810  cardcf  10109  cflim2  10120  intwun  10592  wuncval  10599  inttsk  10631  intgru  10671  gruina  10675  dfrtrcl2  14872  mremre  17410  mrcval  17416  asplss  21184  aspsubrg  21186  toponmre  22350  subbascn  22511  zarclsint  32120  insiga  32403  sigagenval  32406  sigagensiga  32407  dmsigagen  32410  dfon2lem8  34049  dfon2lem9  34050  bj-snmoore  35397  igenval  36332  pclvalN  38166  elrfi  40786  ismrcd1  40790  mzpval  40824  dmmzp  40825  salgenval  44206  intsal  44213