Theorem intex 5314

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 4306	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4927	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3457	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5290	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 18	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1958	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 220	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5282	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4914	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4926	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2812	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2846	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 330	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2985	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 212	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 209   = wceq 1568  ∃wex 1807   ∈ wcel 2141   ≠ wne 2956  Vcvv 3453   ⊆ wss 3904  ∅c0 4285  ∩ cint 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5256

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-dif 3907  df-in 3911  df-ss 3921  df-nul 4286  df-int 4912

This theorem is referenced by:  intnex  5315  intexab  5316  iinexg  5318  onint0  7789  onintrab  7794  onmindif2  7805  fival  9371  elfi2  9373  elfir  9374  dffi2  9382  elfiun  9389  fifo  9391  tz9.1c  9698  tz9.12lem1  9758  tz9.12lem3  9760  rankf  9765  cardf2  9928  cardval3  9937  cardid2  9938  cardcf  10234  cflim2  10246  intwun  10719  wuncval  10726  inttsk  10758  intgru  10798  gruina  10802  dfrtrcl2  15099  mremre  17655  mrcval  17665  asplss  22002  aspsubrg  22004  toponmre  23229  subbascn  23390  zarclsint  34228  insiga  34493  sigagenval  34496  sigagensiga  34497  dmsigagen  34500  dfon2lem8  36246  dfon2lem9  36247  bj-snmoore  37721  igenval  38678  pclvalN  40632  elrfi  43395  ismrcd1  43399  mzpval  43433  dmmzp  43434  oninfex2  43942  salgenval  47005  intsal  47014