Theorem intex 5313

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 3458	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5290	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 18	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1959	. . 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 2813	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2847	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 330	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2986	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 212	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569  ∃wex 1808   ∈ wcel 2142   ≠ wne 2957  Vcvv 3454   ⊆ wss 3904  ∅c0 4285  ∩ cint 4911

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-in 3911  df-ss 3921  df-nul 4286  df-int 4912

This theorem is used by:  intnex  5314  intexab  5315  iinexg  5317  onint0  7788  onintrab  7793  onmindif2  7804  fival  9370  elfi2  9372  elfir  9373  dffi2  9381  elfiun  9388  fifo  9390  tz9.1c  9697  tz9.12lem1  9757  tz9.12lem3  9759  rankf  9764  cardf2  9936  cardval3  9945  cardid2  9946  cardcf  10241  cflim2  10253  intwun  10726  wuncval  10733  inttsk  10765  intgru  10805  gruina  10809  dfrtrcl2  15106  mremre  17662  mrcval  17672  asplss  22034  aspsubrg  22036  toponmre  23261  subbascn  23422  zarclsint  34271  insiga  34536  sigagenval  34539  sigagensiga  34540  dmsigagen  34543  dfon2lem8  36288  dfon2lem9  36289  bj-snmoore  37783  igenval  38740  pclvalN  40692  elrfi  43453  ismrcd1  43457  mzpval  43491  dmmzp  43492  oninfex2  44000  salgenval  47063  intsal  47072