Theorem intex 5338

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 4347	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4968	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3479	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5322	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1934	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 216	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5316	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4954	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4967	. . . . . 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 3949  ∅c0 4323  ∩ cint 4951

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 5300

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 3952  df-in 3956  df-ss 3966  df-nul 4324  df-int 4952

This theorem is referenced by:  intnex  5339  intexab  5340  iinexg  5342  onint0  7779  onintrab  7784  onmindif2  7795  fival  9407  elfi2  9409  elfir  9410  dffi2  9418  elfiun  9425  fifo  9427  tz9.1c  9725  tz9.12lem1  9782  tz9.12lem3  9784  rankf  9789  cardf2  9938  cardval3  9947  cardid2  9948  cardcf  10247  cflim2  10258  intwun  10730  wuncval  10737  inttsk  10769  intgru  10809  gruina  10813  dfrtrcl2  15009  mremre  17548  mrcval  17554  asplss  21428  aspsubrg  21430  toponmre  22597  subbascn  22758  zarclsint  32852  insiga  33135  sigagenval  33138  sigagensiga  33139  dmsigagen  33142  dfon2lem8  34762  dfon2lem9  34763  bj-snmoore  35994  igenval  36929  pclvalN  38761  elrfi  41432  ismrcd1  41436  mzpval  41470  dmmzp  41471  oninfex2  41994  salgenval  45037  intsal  45046