Theorem intex 5286

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 4916	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3442	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5263	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1930	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 217	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5257	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4902	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4915	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2780	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2813	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 327	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2954	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 209	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2925  Vcvv 3438   ⊆ wss 3905  ∅c0 4286  ∩ cint 4899

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 2701  ax-sep 5238

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-in 3912  df-ss 3922  df-nul 4287  df-int 4900

This theorem is referenced by:  intnex  5287  intexab  5288  iinexg  5290  onint0  7731  onintrab  7736  onmindif2  7747  fival  9321  elfi2  9323  elfir  9324  dffi2  9332  elfiun  9339  fifo  9341  tz9.1c  9645  tz9.12lem1  9702  tz9.12lem3  9704  rankf  9709  cardf2  9858  cardval3  9867  cardid2  9868  cardcf  10165  cflim2  10176  intwun  10648  wuncval  10655  inttsk  10687  intgru  10727  gruina  10731  dfrtrcl2  14987  mremre  17524  mrcval  17534  asplss  21799  aspsubrg  21801  toponmre  22996  subbascn  23157  zarclsint  33838  insiga  34103  sigagenval  34106  sigagensiga  34107  dmsigagen  34110  dfon2lem8  35763  dfon2lem9  35764  bj-snmoore  37086  igenval  38040  pclvalN  39869  elrfi  42667  ismrcd1  42671  mzpval  42705  dmmzp  42706  oninfex2  43218  salgenval  46303  intsal  46312