Theorem intex 5215

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 4247	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4860	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3402	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5199	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1938	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 220	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5193	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4848	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4859	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2787	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2815	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 330	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2961	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 212	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 209   = wceq 1543  ∃wex 1787   ∈ wcel 2112   ≠ wne 2932  Vcvv 3398   ⊆ wss 3853  ∅c0 4223  ∩ cint 4845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ne 2933  df-ral 3056  df-rab 3060  df-v 3400  df-dif 3856  df-in 3860  df-ss 3870  df-nul 4224  df-int 4846

This theorem is referenced by:  intnex  5216  intexab  5217  iinexg  5219  onint0  7553  onintrab  7558  onmindif2  7569  fival  9006  elfi2  9008  elfir  9009  dffi2  9017  elfiun  9024  fifo  9026  tz9.1c  9324  tz9.12lem1  9368  tz9.12lem3  9370  rankf  9375  cardf2  9524  cardval3  9533  cardid2  9534  cardcf  9831  cflim2  9842  intwun  10314  wuncval  10321  inttsk  10353  intgru  10393  gruina  10397  dfrtrcl2  14590  mremre  17061  mrcval  17067  asplss  20787  aspsubrg  20789  toponmre  21944  subbascn  22105  zarclsint  31490  insiga  31771  sigagenval  31774  sigagensiga  31775  dmsigagen  31778  dfon2lem8  33436  dfon2lem9  33437  bj-snmoore  34968  igenval  35905  pclvalN  37590  elrfi  40160  ismrcd1  40164  mzpval  40198  dmmzp  40199  salgenval  43480  intsal  43487