Theorem intex 5312

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 4303	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4926	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3457	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5289	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 18	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1963	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 220	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5281	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4913	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4925	. . . . . 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 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2957  Vcvv 3453   ⊆ wss 3902  ∅c0 4282  ∩ cint 4910

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-in 3909  df-ss 3919  df-nul 4283  df-int 4911

This theorem is used by:  intnex  5313  intexab  5314  iinexg  5316  onint0  7794  onintrab  7799  onmindif2  7810  fival  9386  elfi2  9388  elfir  9389  dffi2  9397  elfiun  9404  fifo  9406  tz9.1c  9713  tz9.12lem1  9773  tz9.12lem3  9775  rankf  9780  cardf2  9952  cardval3  9961  cardid2  9962  cardcf  10257  cflim2  10269  intwun  10748  wuncval  10755  inttsk  10787  intgru  10827  gruina  10831  dfrtrcl2  15139  mremre  17694  mrcval  17704  asplss  22094  aspsubrg  22096  toponmre  23324  subbascn  23485  zarclsint  34390  insiga  34656  sigagenval  34659  sigagensiga  34660  dmsigagen  34663  dfon2lem8  36375  dfon2lem9  36376  bj-snmoore  37871  igenval  38819  pclvalN  40771  elrfi  43547  ismrcd1  43551  mzpval  43585  dmmzp  43586  oninfex2  44094  salgenval  47157  intsal  47166