Theorem intex 5301

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 4318	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4929	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3454	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5278	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1930	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 217	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5272	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4915	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4928	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2781	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2814	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 327	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2955	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 209	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2926  Vcvv 3450   ⊆ wss 3916  ∅c0 4298  ∩ cint 4912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5253

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3919  df-in 3923  df-ss 3933  df-nul 4299  df-int 4913

This theorem is referenced by:  intnex  5302  intexab  5303  iinexg  5305  onint0  7769  onintrab  7774  onmindif2  7785  fival  9369  elfi2  9371  elfir  9372  dffi2  9380  elfiun  9387  fifo  9389  tz9.1c  9689  tz9.12lem1  9746  tz9.12lem3  9748  rankf  9753  cardf2  9902  cardval3  9911  cardid2  9912  cardcf  10211  cflim2  10222  intwun  10694  wuncval  10701  inttsk  10733  intgru  10773  gruina  10777  dfrtrcl2  15034  mremre  17571  mrcval  17577  asplss  21789  aspsubrg  21791  toponmre  22986  subbascn  23147  zarclsint  33868  insiga  34133  sigagenval  34136  sigagensiga  34137  dmsigagen  34140  dfon2lem8  35773  dfon2lem9  35774  bj-snmoore  37096  igenval  38050  pclvalN  39879  elrfi  42675  ismrcd1  42679  mzpval  42713  dmmzp  42714  oninfex2  43227  salgenval  46312  intsal  46321