Theorem intex 4747

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 3890	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4427	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3176	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 4730	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1845	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 206	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 4724	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4413	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4425	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	syl6eq 2660	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2672	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 316	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2811	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 198	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 195   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  Vcvv 3173   ⊆ wss 3540  ∅c0 3874  ∩ cint 4410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554  df-nul 3875  df-int 4411

This theorem is referenced by:  intnex  4748  intexab  4749  iinexg  4751  onint0  6888  onintrab  6893  onmindif2  6904  fival  8201  elfi2  8203  elfir  8204  dffi2  8212  elfiun  8219  fifo  8221  tz9.1c  8489  tz9.12lem1  8533  tz9.12lem3  8535  rankf  8540  cardf2  8652  cardval3  8661  cardid2  8662  cardcf  8957  cflim2  8968  intwun  9436  wuncval  9443  inttsk  9475  intgru  9515  gruina  9519  dfrtrcl2  13650  mremre  16087  mrcval  16093  asplss  19150  aspsubrg  19152  toponmre  20707  subbascn  20868  insiga  29527  sigagenval  29530  sigagensiga  29531  dmsigagen  29534  dfon2lem8  30939  dfon2lem9  30940  igenval  33030  pclvalN  34194  elrfi  36275  ismrcd1  36279  mzpval  36313  dmmzp  36314  salgenval  39217  intsal  39224