Theorem intex 5294

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 4300	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4915	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3452	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5271	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1944	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 219	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5264	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4902	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4914	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2807	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2841	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 329	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2980	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 211	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 208   = wceq 1554  ∃wex 1793   ∈ wcel 2136   ≠ wne 2951  Vcvv 3448   ⊆ wss 3899  ∅c0 4280  ∩ cint 4899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-sep 5240

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ne 2952  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-dif 3902  df-in 3906  df-ss 3916  df-nul 4281  df-int 4900

This theorem is referenced by:  intnex  5295  intexab  5296  iinexg  5298  onint0  7763  onintrab  7768  onmindif2  7779  fival  9348  elfi2  9350  elfir  9351  dffi2  9359  elfiun  9366  fifo  9368  tz9.1c  9675  tz9.12lem1  9735  tz9.12lem3  9737  rankf  9742  cardf2  9891  cardval3  9900  cardid2  9901  cardcf  10198  cflim2  10210  intwun  10683  wuncval  10690  inttsk  10722  intgru  10762  gruina  10766  dfrtrcl2  15065  mremre  17608  mrcval  17618  asplss  21898  aspsubrg  21900  toponmre  23126  subbascn  23287  zarclsint  34123  insiga  34388  sigagenval  34391  sigagensiga  34392  dmsigagen  34395  dfon2lem8  36086  dfon2lem9  36087  bj-snmoore  37551  igenval  38508  pclvalN  40462  elrfi  43223  ismrcd1  43227  mzpval  43261  dmmzp  43262  oninfex2  43770  salgenval  46843  intsal  46852