Theorem intex 5333

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 4342	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4961	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3473	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5315	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1926	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 216	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5309	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4947	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4960	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2783	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2813	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 327	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2965	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 208	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 205   = wceq 1534  ∃wex 1774   ∈ wcel 2099   ≠ wne 2935  Vcvv 3469   ⊆ wss 3944  ∅c0 4318  ∩ cint 4944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-sep 5293

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ne 2936  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-in 3951  df-ss 3961  df-nul 4319  df-int 4945

This theorem is referenced by:  intnex  5334  intexab  5335  iinexg  5337  onint0  7788  onintrab  7793  onmindif2  7804  fival  9427  elfi2  9429  elfir  9430  dffi2  9438  elfiun  9445  fifo  9447  tz9.1c  9745  tz9.12lem1  9802  tz9.12lem3  9804  rankf  9809  cardf2  9958  cardval3  9967  cardid2  9968  cardcf  10267  cflim2  10278  intwun  10750  wuncval  10757  inttsk  10789  intgru  10829  gruina  10833  dfrtrcl2  15033  mremre  17575  mrcval  17581  asplss  21794  aspsubrg  21796  toponmre  22984  subbascn  23145  zarclsint  33409  insiga  33692  sigagenval  33695  sigagensiga  33696  dmsigagen  33699  dfon2lem8  35322  dfon2lem9  35323  bj-snmoore  36528  igenval  37469  pclvalN  39300  elrfi  42036  ismrcd1  42040  mzpval  42074  dmmzp  42075  oninfex2  42596  salgenval  45632  intsal  45641