Theorem intex 5304

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 4299	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4922	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3454	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5281	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 18	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1962	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 220	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5273	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4909	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4921	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2811	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2845	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 330	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2984	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 212	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569  ∃wex 1811   ∈ wcel 2144   ≠ wne 2955  Vcvv 3450   ⊆ wss 3895  ∅c0 4278  ∩ cint 4906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-nul 4279  df-int 4907

This theorem is used by:  intnex  5305  intexab  5306  iinexg  5308  onint0  7805  onintrab  7810  onmindif2  7821  fival  9405  elfi2  9407  elfir  9408  dffi2  9416  elfiun  9423  fifo  9425  tz9.1c  9732  tz9.12lem1  9795  tz9.12lem3  9797  rankf  9803  cardf2  10025  cardval3  10034  cardid2  10035  cardcf  10330  cflim2  10342  intwun  10821  wuncval  10828  inttsk  10860  intgru  10900  gruina  10904  dfrtrcl2  15216  mremre  17775  mrcval  17785  asplss  22182  aspsubrg  22184  toponmre  23412  subbascn  23573  zarclsint  34547  insiga  34813  sigagenval  34816  sigagensiga  34817  dmsigagen  34820  dfon2lem8  36627  dfon2lem9  36628  bj-snmoore  38109  igenval  39071  pclvalN  41023  elrfi  43781  ismrcd1  43785  mzpval  43819  dmmzp  43820  oninfex2  44323  salgenval  47407  intsal  47416