Theorem intex 5309

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 4303	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		intss1 4926	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
3		vex 3458	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5286	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 18	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1965	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 220	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5278	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4913	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4925	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2814	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2849	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 330	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2988	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 212	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2147   ≠ wne 2959  Vcvv 3454   ⊆ wss 3900  ∅c0 4281  ∩ cint 4910

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-nul 4282  df-int 4911

This theorem is used by:  intnex  5310  intexab  5311  iinexg  5313  onint0  7829  onintrab  7834  onmindif2  7845  fival  9431  elfi2  9433  elfir  9434  dffi2  9442  elfiun  9449  fifo  9451  tz9.1c  9758  tz9.12lem1  9821  tz9.12lem3  9823  rankf  9829  cardf2  10051  cardval3  10060  cardid2  10061  cardcf  10356  cflim2  10368  intwun  10847  wuncval  10854  inttsk  10886  intgru  10926  gruina  10930  dfrtrcl2  15244  mremre  17803  mrcval  17813  asplss  22211  aspsubrg  22213  toponmre  23441  subbascn  23602  zarclsint  34574  insiga  34840  sigagenval  34843  sigagensiga  34844  dmsigagen  34847  dfon2lem8  36730  dfon2lem9  36731  bj-snmoore  38225  igenval  39187  pclvalN  41139  elrfi  43898  ismrcd1  43902  mzpval  43936  dmmzp  43937  oninfex2  44439  salgenval  47536  intsal  47545