Theorem intex 5302

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 4319	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4930	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3454	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5279	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1930	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 217	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5273	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4916	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4929	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2781	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2814	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 327	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2955	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 209	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2926  Vcvv 3450   ⊆ wss 3917  ∅c0 4299  ∩ cint 4913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-in 3924  df-ss 3934  df-nul 4300  df-int 4914

This theorem is referenced by:  intnex  5303  intexab  5304  iinexg  5306  onint0  7770  onintrab  7775  onmindif2  7786  fival  9370  elfi2  9372  elfir  9373  dffi2  9381  elfiun  9388  fifo  9390  tz9.1c  9690  tz9.12lem1  9747  tz9.12lem3  9749  rankf  9754  cardf2  9903  cardval3  9912  cardid2  9913  cardcf  10212  cflim2  10223  intwun  10695  wuncval  10702  inttsk  10734  intgru  10774  gruina  10778  dfrtrcl2  15035  mremre  17572  mrcval  17578  asplss  21790  aspsubrg  21792  toponmre  22987  subbascn  23148  zarclsint  33869  insiga  34134  sigagenval  34137  sigagensiga  34138  dmsigagen  34141  dfon2lem8  35785  dfon2lem9  35786  bj-snmoore  37108  igenval  38062  pclvalN  39891  elrfi  42689  ismrcd1  42693  mzpval  42727  dmmzp  42728  oninfex2  43241  salgenval  46326  intsal  46335