Theorem intex 5240

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 4310	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4891	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3497	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5225	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1931	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 219	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5219	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4879	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4890	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	syl6eq 2872	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2897	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 329	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 3045	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 211	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 208   = wceq 1537  ∃wex 1780   ∈ wcel 2114   ≠ wne 3016  Vcvv 3494   ⊆ wss 3936  ∅c0 4291  ∩ cint 4876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rab 3147  df-v 3496  df-dif 3939  df-in 3943  df-ss 3952  df-nul 4292  df-int 4877

This theorem is referenced by:  intnex  5241  intexab  5242  iinexg  5244  onint0  7511  onintrab  7516  onmindif2  7527  fival  8876  elfi2  8878  elfir  8879  dffi2  8887  elfiun  8894  fifo  8896  tz9.1c  9172  tz9.12lem1  9216  tz9.12lem3  9218  rankf  9223  cardf2  9372  cardval3  9381  cardid2  9382  cardcf  9674  cflim2  9685  intwun  10157  wuncval  10164  inttsk  10196  intgru  10236  gruina  10240  dfrtrcl2  14421  mremre  16875  mrcval  16881  asplss  20103  aspsubrg  20105  toponmre  21701  subbascn  21862  insiga  31396  sigagenval  31399  sigagensiga  31400  dmsigagen  31403  dfon2lem8  33035  dfon2lem9  33036  bj-snmoore  34408  igenval  35354  pclvalN  37041  elrfi  39311  ismrcd1  39315  mzpval  39349  dmmzp  39350  salgenval  42626  intsal  42633