Theorem intex 4951

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 4078	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4626	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3354	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 4936	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 2010	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 207	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 4930	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4614	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4625	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	syl6eq 2821	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2835	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 316	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2972	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 199	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 196   = wceq 1631  ∃wex 1852   ∈ wcel 2145   ≠ wne 2943  Vcvv 3351   ⊆ wss 3723  ∅c0 4063  ∩ cint 4611

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-v 3353  df-dif 3726  df-in 3730  df-ss 3737  df-nul 4064  df-int 4612

This theorem is referenced by:  intnex  4952  intexab  4953  iinexg  4955  onint0  7143  onintrab  7148  onmindif2  7159  fival  8474  elfi2  8476  elfir  8477  dffi2  8485  elfiun  8492  fifo  8494  tz9.1c  8770  tz9.12lem1  8814  tz9.12lem3  8816  rankf  8821  cardf2  8969  cardval3  8978  cardid2  8979  cardcf  9276  cflim2  9287  intwun  9759  wuncval  9766  inttsk  9798  intgru  9838  gruina  9842  dfrtrcl2  14010  mremre  16472  mrcval  16478  asplss  19544  aspsubrg  19546  toponmre  21118  subbascn  21279  insiga  30540  sigagenval  30543  sigagensiga  30544  dmsigagen  30547  dfon2lem8  32031  dfon2lem9  32032  bj-snmoore  33400  igenval  34192  pclvalN  35698  elrfi  37783  ismrcd1  37787  mzpval  37821  dmmzp  37822  salgenval  41058  intsal  41065