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

Syntax hints:   ↔ wb 206   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ≠ wne 2930  Vcvv 3438   ⊆ wss 3899  ∅c0 4284  ∩ cint 4899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-in 3906  df-ss 3916  df-nul 4285  df-int 4900

This theorem is referenced by:  intnex  5287  intexab  5288  iinexg  5290  onint0  7733  onintrab  7738  onmindif2  7749  fival  9306  elfi2  9308  elfir  9309  dffi2  9317  elfiun  9324  fifo  9326  tz9.1c  9630  tz9.12lem1  9690  tz9.12lem3  9692  rankf  9697  cardf2  9846  cardval3  9855  cardid2  9856  cardcf  10153  cflim2  10164  intwun  10636  wuncval  10643  inttsk  10675  intgru  10715  gruina  10719  dfrtrcl2  14979  mremre  17516  mrcval  17526  asplss  21821  aspsubrg  21823  toponmre  23018  subbascn  23179  zarclsint  33896  insiga  34161  sigagenval  34164  sigagensiga  34165  dmsigagen  34168  dfon2lem8  35843  dfon2lem9  35844  bj-snmoore  37168  igenval  38111  pclvalN  39999  elrfi  42801  ismrcd1  42805  mzpval  42839  dmmzp  42840  oninfex2  43352  salgenval  46433  intsal  46442