Theorem intex 5290

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 4306	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4919	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3445	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5267	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1932	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 217	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5261	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4906	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4918	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2788	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2822	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 327	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2962	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 209	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 206   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2933  Vcvv 3441   ⊆ wss 3902  ∅c0 4286  ∩ cint 4903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-in 3909  df-ss 3919  df-nul 4287  df-int 4904

This theorem is referenced by:  intnex  5291  intexab  5292  iinexg  5294  onint0  7738  onintrab  7743  onmindif2  7754  fival  9319  elfi2  9321  elfir  9322  dffi2  9330  elfiun  9337  fifo  9339  tz9.1c  9643  tz9.12lem1  9703  tz9.12lem3  9705  rankf  9710  cardf2  9859  cardval3  9868  cardid2  9869  cardcf  10166  cflim2  10177  intwun  10650  wuncval  10657  inttsk  10689  intgru  10729  gruina  10733  dfrtrcl2  14989  mremre  17527  mrcval  17537  asplss  21833  aspsubrg  21835  toponmre  23041  subbascn  23202  zarclsint  34010  insiga  34275  sigagenval  34278  sigagensiga  34279  dmsigagen  34282  dfon2lem8  35963  dfon2lem9  35964  bj-snmoore  37289  igenval  38233  pclvalN  40187  elrfi  42972  ismrcd1  42976  mzpval  43010  dmmzp  43011  oninfex2  43523  salgenval  46601  intsal  46610