Theorem intex 5299

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 4316	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4927	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3451	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5276	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1930	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 217	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5270	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4913	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4926	. . . . . 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 3447   ⊆ wss 3914  ∅c0 4296  ∩ cint 4910

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 5251

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 3406  df-v 3449  df-dif 3917  df-in 3921  df-ss 3931  df-nul 4297  df-int 4911

This theorem is referenced by:  intnex  5300  intexab  5301  iinexg  5303  onint0  7767  onintrab  7772  onmindif2  7783  fival  9363  elfi2  9365  elfir  9366  dffi2  9374  elfiun  9381  fifo  9383  tz9.1c  9683  tz9.12lem1  9740  tz9.12lem3  9742  rankf  9747  cardf2  9896  cardval3  9905  cardid2  9906  cardcf  10205  cflim2  10216  intwun  10688  wuncval  10695  inttsk  10727  intgru  10767  gruina  10771  dfrtrcl2  15028  mremre  17565  mrcval  17571  asplss  21783  aspsubrg  21785  toponmre  22980  subbascn  23141  zarclsint  33862  insiga  34127  sigagenval  34130  sigagensiga  34131  dmsigagen  34134  dfon2lem8  35778  dfon2lem9  35779  bj-snmoore  37101  igenval  38055  pclvalN  39884  elrfi  42682  ismrcd1  42686  mzpval  42720  dmmzp  42721  oninfex2  43234  salgenval  46319  intsal  46328