Theorem intex 5337

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 4346	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4967	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3479	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5321	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1934	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 216	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5315	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4953	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4966	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2789	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2819	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 327	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2971	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 208	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 205   = wceq 1542  ∃wex 1782   ∈ wcel 2107   ≠ wne 2941  Vcvv 3475   ⊆ wss 3948  ∅c0 4322  ∩ cint 4950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5299

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-in 3955  df-ss 3965  df-nul 4323  df-int 4951

This theorem is referenced by:  intnex  5338  intexab  5339  iinexg  5341  onint0  7776  onintrab  7781  onmindif2  7792  fival  9404  elfi2  9406  elfir  9407  dffi2  9415  elfiun  9422  fifo  9424  tz9.1c  9722  tz9.12lem1  9779  tz9.12lem3  9781  rankf  9786  cardf2  9935  cardval3  9944  cardid2  9945  cardcf  10244  cflim2  10255  intwun  10727  wuncval  10734  inttsk  10766  intgru  10806  gruina  10810  dfrtrcl2  15006  mremre  17545  mrcval  17551  asplss  21420  aspsubrg  21422  toponmre  22589  subbascn  22750  zarclsint  32841  insiga  33124  sigagenval  33127  sigagensiga  33128  dmsigagen  33131  dfon2lem8  34751  dfon2lem9  34752  bj-snmoore  35983  igenval  36918  pclvalN  38750  elrfi  41418  ismrcd1  41422  mzpval  41456  dmmzp  41457  oninfex2  41980  salgenval  45024  intsal  45033