Theorem intex 5279

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 4288	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4900	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3436	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5256	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1937	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 218	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5249	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4887	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4899	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2791	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2825	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 328	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2964	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 210	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 207   = wceq 1547  ∃wex 1786   ∈ wcel 2119   ≠ wne 2935  Vcvv 3432   ⊆ wss 3890  ∅c0 4268  ∩ cint 4884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-in 3897  df-ss 3907  df-nul 4269  df-int 4885

This theorem is referenced by:  intnex  5280  intexab  5281  iinexg  5283  onint0  7741  onintrab  7746  onmindif2  7757  fival  9322  elfi2  9324  elfir  9325  dffi2  9333  elfiun  9340  fifo  9342  tz9.1c  9649  tz9.12lem1  9709  tz9.12lem3  9711  rankf  9716  cardf2  9865  cardval3  9874  cardid2  9875  cardcf  10172  cflim2  10183  intwun  10656  wuncval  10663  inttsk  10695  intgru  10735  gruina  10739  dfrtrcl2  15022  mremre  17564  mrcval  17574  asplss  21855  aspsubrg  21857  toponmre  23083  subbascn  23244  zarclsint  34063  insiga  34328  sigagenval  34331  sigagensiga  34332  dmsigagen  34335  dfon2lem8  36017  dfon2lem9  36018  bj-snmoore  37472  igenval  38429  pclvalN  40383  elrfi  43144  ismrcd1  43148  mzpval  43182  dmmzp  43183  oninfex2  43691  salgenval  46765  intsal  46774