Theorem intex 5291

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 4307	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4920	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3446	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5268	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1932	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 217	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5262	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4907	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4919	. . . . . 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 3442   ⊆ wss 3903  ∅c0 4287  ∩ cint 4904

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 5243

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 3063  df-rab 3402  df-v 3444  df-dif 3906  df-in 3910  df-ss 3920  df-nul 4288  df-int 4905

This theorem is referenced by:  intnex  5292  intexab  5293  iinexg  5295  onint0  7746  onintrab  7751  onmindif2  7762  fival  9327  elfi2  9329  elfir  9330  dffi2  9338  elfiun  9345  fifo  9347  tz9.1c  9651  tz9.12lem1  9711  tz9.12lem3  9713  rankf  9718  cardf2  9867  cardval3  9876  cardid2  9877  cardcf  10174  cflim2  10185  intwun  10658  wuncval  10665  inttsk  10697  intgru  10737  gruina  10741  dfrtrcl2  14997  mremre  17535  mrcval  17545  asplss  21841  aspsubrg  21843  toponmre  23049  subbascn  23210  zarclsint  34049  insiga  34314  sigagenval  34317  sigagensiga  34318  dmsigagen  34321  dfon2lem8  36001  dfon2lem9  36002  bj-snmoore  37357  igenval  38301  pclvalN  40255  elrfi  43040  ismrcd1  43044  mzpval  43078  dmmzp  43079  oninfex2  43591  salgenval  46668  intsal  46677