Theorem intex 4603

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 3794	. . 3 |- ( A =/= (/) <-> E. x x e. A )
2		intss1 4297	. . . . 5 |- ( x e. A -> |^| A C_ x )
3		vex 3116	. . . . . 6 |- x e. _V
4	3	ssex 4591	. . . . 5 |- ( |^| A C_ x -> |^| A e. _V )
5	2, 4	syl 16	. . . 4 |- ( x e. A -> |^| A e. _V )
6	5	exlimiv 1698	. . 3 |- ( E. x x e. A -> |^| A e. _V )
7	1, 6	sylbi 195	. 2 |- ( A =/= (/) -> |^| A e. _V )
8		vprc 4585	. . . 4 |- -. _V e. _V
9		inteq 4285	. . . . . 6 |- ( A = (/) -> |^| A = |^| (/) )
10		int0 4296	. . . . . 6 |- |^| (/) = _V
11	9, 10	syl6eq 2524	. . . . 5 |- ( A = (/) -> |^| A = _V )
12	11	eleq1d 2536	. . . 4 |- ( A = (/) -> ( |^| A e. _V <-> _V e. _V ) )
13	8, 12	mtbiri 303	. . 3 |- ( A = (/) -> -. |^| A e. _V )
14	13	necon2ai 2702	. 2 |- ( |^| A e. _V -> A =/= (/) )
15	7, 14	impbii 188	1 |- ( A =/= (/) <-> |^| A e. _V )

Syntax hints:   <-> wb 184   = wceq 1379   E.wex 1596   e. wcel 1767   =/= wne 2662   _Vcvv 3113   C_ wss 3476   (/)c0 3785   |^|cint 4282

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-v 3115  df-dif 3479  df-in 3483  df-ss 3490  df-nul 3786  df-int 4283

This theorem is referenced by:  intnex  4604  intexab  4605  iinexg  4607  onint0  6610  onintrab  6615  onmindif2  6626  fival  7871  elfi2  7873  elfir  7874  dffi2  7882  elfiun  7889  fifo  7891  tz9.1c  8160  tz9.12lem1  8204  tz9.12lem3  8206  rankf  8211  cardf2  8323  cardval3  8332  cardid2  8333  cardcf  8631  cflim2  8642  intwun  9112  wuncval  9119  inttsk  9151  intgru  9191  gruina  9195  mremre  14858  mrcval  14864  asplss  17765  aspsubrg  17767  toponmre  19376  subbascn  19537  insiga  27793  sigagenval  27796  sigagensiga  27797  dmsigagen  27800  dfrtrcl2  28562  dfon2lem8  28815  dfon2lem9  28816  igenval  30077  elrfi  30246  ismrcd1  30250  mzpval  30284  dmmzp  30285  pclvalN  34695