Theorem intex 4978

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 4095	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4648	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3353	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 4963	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 2025	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 208	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 4958	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4636	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4647	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	syl6eq 2815	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2829	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 318	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2966	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 200	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

Syntax hints:   ↔ wb 197   = wceq 1652  ∃wex 1874   ∈ wcel 2155   ≠ wne 2937  Vcvv 3350   ⊆ wss 3732  ∅c0 4079  ∩ cint 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-v 3352  df-dif 3735  df-in 3739  df-ss 3746  df-nul 4080  df-int 4634

This theorem is referenced by:  intnex  4979  intexab  4980  iinexg  4982  onint0  7194  onintrab  7199  onmindif2  7210  fival  8525  elfi2  8527  elfir  8528  dffi2  8536  elfiun  8543  fifo  8545  tz9.1c  8821  tz9.12lem1  8865  tz9.12lem3  8867  rankf  8872  cardf2  9020  cardval3  9029  cardid2  9030  cardcf  9327  cflim2  9338  intwun  9810  wuncval  9817  inttsk  9849  intgru  9889  gruina  9893  dfrtrcl2  14089  mremre  16532  mrcval  16538  asplss  19603  aspsubrg  19605  toponmre  21177  subbascn  21338  insiga  30582  sigagenval  30585  sigagensiga  30586  dmsigagen  30589  dfon2lem8  32070  dfon2lem9  32071  bj-snmoore  33428  igenval  34214  pclvalN  35778  elrfi  37867  ismrcd1  37871  mzpval  37905  dmmzp  37906  salgenval  41110  intsal  41117