Theorem intex 5350

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 4359	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4968	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3482	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5327	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1928	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 217	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5321	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4954	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4967	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2791	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2824	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 327	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2968	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 209	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 206   = wceq 1537  ∃wex 1776   ∈ wcel 2106   ≠ wne 2938  Vcvv 3478   ⊆ wss 3963  ∅c0 4339  ∩ cint 4951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-in 3970  df-ss 3980  df-nul 4340  df-int 4952

This theorem is referenced by:  intnex  5351  intexab  5352  iinexg  5354  onint0  7811  onintrab  7816  onmindif2  7827  fival  9450  elfi2  9452  elfir  9453  dffi2  9461  elfiun  9468  fifo  9470  tz9.1c  9768  tz9.12lem1  9825  tz9.12lem3  9827  rankf  9832  cardf2  9981  cardval3  9990  cardid2  9991  cardcf  10290  cflim2  10301  intwun  10773  wuncval  10780  inttsk  10812  intgru  10852  gruina  10856  dfrtrcl2  15098  mremre  17649  mrcval  17655  asplss  21912  aspsubrg  21914  toponmre  23117  subbascn  23278  zarclsint  33833  insiga  34118  sigagenval  34121  sigagensiga  34122  dmsigagen  34125  dfon2lem8  35772  dfon2lem9  35773  bj-snmoore  37096  igenval  38048  pclvalN  39873  elrfi  42682  ismrcd1  42686  mzpval  42720  dmmzp  42721  oninfex2  43234  salgenval  46277  intsal  46286