Theorem intex 5280

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 4301	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4911	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3438	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5257	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1931	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 217	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5251	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4898	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4910	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2781	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2814	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 327	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2955	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 209	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 206   = wceq 1541  ∃wex 1780   ∈ wcel 2110   ≠ wne 2926  Vcvv 3434   ⊆ wss 3900  ∅c0 4281  ∩ cint 4895

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 2112  ax-9 2120  ax-ext 2702  ax-sep 5232

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 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-dif 3903  df-in 3907  df-ss 3917  df-nul 4282  df-int 4896

This theorem is referenced by:  intnex  5281  intexab  5282  iinexg  5284  onint0  7719  onintrab  7724  onmindif2  7735  fival  9291  elfi2  9293  elfir  9294  dffi2  9302  elfiun  9309  fifo  9311  tz9.1c  9615  tz9.12lem1  9672  tz9.12lem3  9674  rankf  9679  cardf2  9828  cardval3  9837  cardid2  9838  cardcf  10135  cflim2  10146  intwun  10618  wuncval  10625  inttsk  10657  intgru  10697  gruina  10701  dfrtrcl2  14961  mremre  17498  mrcval  17508  asplss  21804  aspsubrg  21806  toponmre  23001  subbascn  23162  zarclsint  33875  insiga  34140  sigagenval  34143  sigagensiga  34144  dmsigagen  34147  dfon2lem8  35803  dfon2lem9  35804  bj-snmoore  37126  igenval  38080  pclvalN  39908  elrfi  42706  ismrcd1  42710  mzpval  42744  dmmzp  42745  oninfex2  43257  salgenval  46338  intsal  46347