Theorem intex 5304

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 4299	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4922	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3454	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5281	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 18	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1963	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 220	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5273	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4909	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4921	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2811	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2845	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 330	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2984	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 212	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2955  Vcvv 3450   ⊆ wss 3898  ∅c0 4278  ∩ cint 4906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3901  df-in 3905  df-ss 3915  df-nul 4279  df-int 4907

This theorem is used by:  intnex  5305  intexab  5306  iinexg  5308  onint0  7788  onintrab  7793  onmindif2  7804  fival  9382  elfi2  9384  elfir  9385  dffi2  9393  elfiun  9400  fifo  9402  tz9.1c  9709  tz9.12lem1  9769  tz9.12lem3  9771  rankf  9776  cardf2  9996  cardval3  10005  cardid2  10006  cardcf  10301  cflim2  10313  intwun  10792  wuncval  10799  inttsk  10831  intgru  10871  gruina  10875  dfrtrcl2  15183  mremre  17736  mrcval  17746  asplss  22143  aspsubrg  22145  toponmre  23373  subbascn  23534  zarclsint  34438  insiga  34704  sigagenval  34707  sigagensiga  34708  dmsigagen  34711  dfon2lem8  36474  dfon2lem9  36475  bj-snmoore  37954  igenval  38915  pclvalN  40867  elrfi  43643  ismrcd1  43647  mzpval  43681  dmmzp  43682  oninfex2  44190  salgenval  47253  intsal  47262