Theorem intex 5312

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 3457	. . . . . 6 ⊢ 𝑥 ∈ V
4	3	ssex 5289	. . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V)
5	2, 4	syl 18	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
6	5	exlimiv 1963	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
7	1, 6	sylbi 220	. 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
8		vprc 5281	. . . 4 ⊢ ¬ V ∈ V
9		inteq 4913	. . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
10		int0 4925	. . . . . 6 ⊢ ∩ ∅ = V
11	9, 10	eqtrdi 2813	. . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V)
12	11	eleq1d 2847	. . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V))
13	8, 12	mtbiri 330	. . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V)
14	13	necon2ai 2986	. 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
15	7, 14	impbii 212	1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2957  Vcvv 3453   ⊆ wss 3902  ∅c0 4282  ∩ 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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255

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 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-in 3909  df-ss 3919  df-nul 4283  df-int 4911

This theorem is used by:  intnex  5313  intexab  5314  iinexg  5316  onint0  7793  onintrab  7798  onmindif2  7809  fival  9385  elfi2  9387  elfir  9388  dffi2  9396  elfiun  9403  fifo  9405  tz9.1c  9712  tz9.12lem1  9772  tz9.12lem3  9774  rankf  9779  cardf2  9951  cardval3  9960  cardid2  9961  cardcf  10256  cflim2  10268  intwun  10747  wuncval  10754  inttsk  10786  intgru  10826  gruina  10830  dfrtrcl2  15137  mremre  17692  mrcval  17702  asplss  22092  aspsubrg  22094  toponmre  23322  subbascn  23483  zarclsint  34384  insiga  34650  sigagenval  34653  sigagensiga  34654  dmsigagen  34657  dfon2lem8  36369  dfon2lem9  36370  bj-snmoore  37865  igenval  38813  pclvalN  40765  elrfi  43541  ismrcd1  43545  mzpval  43579  dmmzp  43580  oninfex2  44088  salgenval  47151  intsal  47160