Theorem intex 4573

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	|- ( A =/= (/) <-> |^| A e. _V )

Proof of Theorem intex

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		n0 3753	. . 3 |- ( A =/= (/) <-> E. x x e. A )
2		intss1 4263	. . . . 5 |- ( x e. A -> |^| A C_ x )
3		vex 3060	. . . . . 6 |- x e. _V
4	3	ssex 4561	. . . . 5 |- ( |^| A C_ x -> |^| A e. _V )
5	2, 4	syl 17	. . . 4 |- ( x e. A -> |^| A e. _V )
6	5	exlimiv 1787	. . 3 |- ( E. x x e. A -> |^| A e. _V )
7	1, 6	sylbi 200	. 2 |- ( A =/= (/) -> |^| A e. _V )
8		vprc 4555	. . . 4 |- -. _V e. _V
9		inteq 4251	. . . . . 6 |- ( A = (/) -> |^| A = |^| (/) )
10		int0 4262	. . . . . 6 |- |^| (/) = _V
11	9, 10	syl6eq 2512	. . . . 5 |- ( A = (/) -> |^| A = _V )
12	11	eleq1d 2524	. . . 4 |- ( A = (/) -> ( |^| A e. _V <-> _V e. _V ) )
13	8, 12	mtbiri 309	. . 3 |- ( A = (/) -> -. |^| A e. _V )
14	13	necon2ai 2665	. 2 |- ( |^| A e. _V -> A =/= (/) )
15	7, 14	impbii 192	1 |- ( A =/= (/) <-> |^| A e. _V )

Syntax hints:   <-> wb 189   = wceq 1455   E.wex 1674   e. wcel 1898   =/= wne 2633   _Vcvv 3057   C_ wss 3416   (/)c0 3743   |^|cint 4248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-v 3059  df-dif 3419  df-in 3423  df-ss 3430  df-nul 3744  df-int 4249

This theorem is referenced by:  intnex  4574  intexab  4575  iinexg  4577  onint0  6650  onintrab  6655  onmindif2  6666  fival  7952  elfi2  7954  elfir  7955  dffi2  7963  elfiun  7970  fifo  7972  tz9.1c  8240  tz9.12lem1  8284  tz9.12lem3  8286  rankf  8291  cardf2  8403  cardval3  8412  cardid2  8413  cardcf  8708  cflim2  8719  intwun  9186  wuncval  9193  inttsk  9225  intgru  9265  gruina  9269  dfrtrcl2  13174  mremre  15559  mrcval  15565  asplss  18602  aspsubrg  18604  toponmre  20158  subbascn  20319  insiga  29008  sigagenval  29011  sigagensiga  29012  dmsigagen  29015  dfon2lem8  30485  dfon2lem9  30486  igenval  32339  pclvalN  33500  elrfi  35581  ismrcd1  35585  mzpval  35619  dmmzp  35620  salgenval  38220  intsal  38227