Theorem intex 5305

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 4308	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4924	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3461	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5282	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 18	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1953	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 220	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5275	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4911	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4923	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2816	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2850	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 330	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2989	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 212	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 209   = wceq 1563  ∃wex 1802   ∈ wcel 2145   ≠ wne 2960  Vcvv 3457   ⊆ wss 3907  ∅c0 4288  ∩ cint 4908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-in 3914  df-ss 3924  df-nul 4289  df-int 4909

This theorem is referenced by:  intnex  5306  intexab  5307  iinexg  5309  onint0  7778  onintrab  7783  onmindif2  7794  fival  9360  elfi2  9362  elfir  9363  dffi2  9371  elfiun  9378  fifo  9380  tz9.1c  9687  tz9.12lem1  9747  tz9.12lem3  9749  rankf  9754  cardf2  9917  cardval3  9926  cardid2  9927  cardcf  10223  cflim2  10235  intwun  10708  wuncval  10715  inttsk  10747  intgru  10787  gruina  10791  dfrtrcl2  15089  mremre  17646  mrcval  17656  asplss  21983  aspsubrg  21985  toponmre  23211  subbascn  23372  zarclsint  34179  insiga  34444  sigagenval  34447  sigagensiga  34448  dmsigagen  34451  dfon2lem8  36151  dfon2lem9  36152  bj-snmoore  37615  igenval  38572  pclvalN  40526  elrfi  43287  ismrcd1  43291  mzpval  43325  dmmzp  43326  oninfex2  43834  salgenval  46893  intsal  46902