Theorem intex 5344

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 4349	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4971	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3466	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5326	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1926	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 216	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5320	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4957	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4970	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2782	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2811	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 326	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2960	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 208	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 205   = wceq 1534  ∃wex 1774   ∈ wcel 2099   ≠ wne 2930  Vcvv 3462   ⊆ wss 3947  ∅c0 4325  ∩ cint 4954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5304

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-in 3954  df-ss 3964  df-nul 4326  df-int 4955

This theorem is referenced by:  intnex  5345  intexab  5346  iinexg  5348  onint0  7800  onintrab  7805  onmindif2  7816  fival  9455  elfi2  9457  elfir  9458  dffi2  9466  elfiun  9473  fifo  9475  tz9.1c  9773  tz9.12lem1  9830  tz9.12lem3  9832  rankf  9837  cardf2  9986  cardval3  9995  cardid2  9996  cardcf  10295  cflim2  10306  intwun  10778  wuncval  10785  inttsk  10817  intgru  10857  gruina  10861  dfrtrcl2  15067  mremre  17617  mrcval  17623  asplss  21871  aspsubrg  21873  toponmre  23088  subbascn  23249  zarclsint  33687  insiga  33970  sigagenval  33973  sigagensiga  33974  dmsigagen  33977  dfon2lem8  35614  dfon2lem9  35615  bj-snmoore  36820  igenval  37762  pclvalN  39589  elrfi  42351  ismrcd1  42355  mzpval  42389  dmmzp  42390  oninfex2  42910  salgenval  45942  intsal  45951