Theorem intex 5362

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 4376	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4987	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3492	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5339	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1929	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 217	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5333	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4973	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4986	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2796	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2829	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 327	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2976	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 209	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 206   = wceq 1537  ∃wex 1777   ∈ wcel 2108   ≠ wne 2946  Vcvv 3488   ⊆ wss 3976  ∅c0 4352  ∩ cint 4970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-in 3983  df-ss 3993  df-nul 4353  df-int 4971

This theorem is referenced by:  intnex  5363  intexab  5364  iinexg  5366  onint0  7827  onintrab  7832  onmindif2  7843  fival  9481  elfi2  9483  elfir  9484  dffi2  9492  elfiun  9499  fifo  9501  tz9.1c  9799  tz9.12lem1  9856  tz9.12lem3  9858  rankf  9863  cardf2  10012  cardval3  10021  cardid2  10022  cardcf  10321  cflim2  10332  intwun  10804  wuncval  10811  inttsk  10843  intgru  10883  gruina  10887  dfrtrcl2  15111  mremre  17662  mrcval  17668  asplss  21917  aspsubrg  21919  toponmre  23122  subbascn  23283  zarclsint  33818  insiga  34101  sigagenval  34104  sigagensiga  34105  dmsigagen  34108  dfon2lem8  35754  dfon2lem9  35755  bj-snmoore  37079  igenval  38021  pclvalN  39847  elrfi  42650  ismrcd1  42654  mzpval  42688  dmmzp  42689  oninfex2  43206  salgenval  46242  intsal  46251