Theorem intex 5256

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 4277	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4891	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3426	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5240	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1934	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 216	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5234	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4879	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4890	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2795	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2823	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 326	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2972	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 208	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 205   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942  Vcvv 3422   ⊆ wss 3883  ∅c0 4253  ∩ cint 4876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rab 3072  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900  df-nul 4254  df-int 4877

This theorem is referenced by:  intnex  5257  intexab  5258  iinexg  5260  onint0  7618  onintrab  7623  onmindif2  7634  fival  9101  elfi2  9103  elfir  9104  dffi2  9112  elfiun  9119  fifo  9121  tz9.1c  9419  tz9.12lem1  9476  tz9.12lem3  9478  rankf  9483  cardf2  9632  cardval3  9641  cardid2  9642  cardcf  9939  cflim2  9950  intwun  10422  wuncval  10429  inttsk  10461  intgru  10501  gruina  10505  dfrtrcl2  14701  mremre  17230  mrcval  17236  asplss  20988  aspsubrg  20990  toponmre  22152  subbascn  22313  zarclsint  31724  insiga  32005  sigagenval  32008  sigagensiga  32009  dmsigagen  32012  dfon2lem8  33672  dfon2lem9  33673  bj-snmoore  35211  igenval  36146  pclvalN  37831  elrfi  40432  ismrcd1  40436  mzpval  40470  dmmzp  40471  salgenval  43752  intsal  43759