Theorem intex 4820

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 3931	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4492	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3203	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 4802	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1858	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 207	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 4796	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4478	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4490	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	syl6eq 2672	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2686	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 317	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2823	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 199	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 196   = wceq 1483  ∃wex 1704   ∈ wcel 1990   ≠ wne 2794  Vcvv 3200   ⊆ wss 3574  ∅c0 3915  ∩ cint 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916  df-int 4476

This theorem is referenced by:  intnex  4821  intexab  4822  iinexg  4824  onint0  6996  onintrab  7001  onmindif2  7012  fival  8318  elfi2  8320  elfir  8321  dffi2  8329  elfiun  8336  fifo  8338  tz9.1c  8606  tz9.12lem1  8650  tz9.12lem3  8652  rankf  8657  cardf2  8769  cardval3  8778  cardid2  8779  cardcf  9074  cflim2  9085  intwun  9557  wuncval  9564  inttsk  9596  intgru  9636  gruina  9640  dfrtrcl2  13802  mremre  16264  mrcval  16270  asplss  19329  aspsubrg  19331  toponmre  20897  subbascn  21058  insiga  30200  sigagenval  30203  sigagensiga  30204  dmsigagen  30207  dfon2lem8  31695  dfon2lem9  31696  bj-snmoore  33068  igenval  33860  pclvalN  35176  elrfi  37257  ismrcd1  37261  mzpval  37295  dmmzp  37296  salgenval  40541  intsal  40548