Theorem intex 5261

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 4280	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4894	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3436	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5245	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1933	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 216	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5239	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4882	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4893	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2794	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2823	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 327	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2973	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 208	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 205   = wceq 1539  ∃wex 1782   ∈ wcel 2106   ≠ wne 2943  Vcvv 3432   ⊆ wss 3887  ∅c0 4256  ∩ cint 4879

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rab 3073  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904  df-nul 4257  df-int 4880

This theorem is referenced by:  intnex  5262  intexab  5263  iinexg  5265  onint0  7641  onintrab  7646  onmindif2  7657  fival  9171  elfi2  9173  elfir  9174  dffi2  9182  elfiun  9189  fifo  9191  tz9.1c  9488  tz9.12lem1  9545  tz9.12lem3  9547  rankf  9552  cardf2  9701  cardval3  9710  cardid2  9711  cardcf  10008  cflim2  10019  intwun  10491  wuncval  10498  inttsk  10530  intgru  10570  gruina  10574  dfrtrcl2  14773  mremre  17313  mrcval  17319  asplss  21078  aspsubrg  21080  toponmre  22244  subbascn  22405  zarclsint  31822  insiga  32105  sigagenval  32108  sigagensiga  32109  dmsigagen  32112  dfon2lem8  33766  dfon2lem9  33767  bj-snmoore  35284  igenval  36219  pclvalN  37904  elrfi  40516  ismrcd1  40520  mzpval  40554  dmmzp  40555  salgenval  43862  intsal  43869