Theorem intex 4448

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 3646	. . 3 |- ( A =/= (/) <-> E. x x e. A )
2		intss1 4143	. . . . 5 |- ( x e. A -> |^| A C_ x )
3		vex 2975	. . . . . 6 |- x e. _V
4	3	ssex 4436	. . . . 5 |- ( |^| A C_ x -> |^| A e. _V )
5	2, 4	syl 16	. . . 4 |- ( x e. A -> |^| A e. _V )
6	5	exlimiv 1688	. . 3 |- ( E. x x e. A -> |^| A e. _V )
7	1, 6	sylbi 195	. 2 |- ( A =/= (/) -> |^| A e. _V )
8		vprc 4430	. . . 4 |- -. _V e. _V
9		inteq 4131	. . . . . 6 |- ( A = (/) -> |^| A = |^| (/) )
10		int0 4142	. . . . . 6 |- |^| (/) = _V
11	9, 10	syl6eq 2491	. . . . 5 |- ( A = (/) -> |^| A = _V )
12	11	eleq1d 2509	. . . 4 |- ( A = (/) -> ( |^| A e. _V <-> _V e. _V ) )
13	8, 12	mtbiri 303	. . 3 |- ( A = (/) -> -. |^| A e. _V )
14	13	necon2ai 2656	. 2 |- ( |^| A e. _V -> A =/= (/) )
15	7, 14	impbii 188	1 |- ( A =/= (/) <-> |^| A e. _V )

Syntax hints:   <-> wb 184   = wceq 1369   E.wex 1586   e. wcel 1756   =/= wne 2606   _Vcvv 2972   C_ wss 3328   (/)c0 3637   |^|cint 4128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-v 2974  df-dif 3331  df-in 3335  df-ss 3342  df-nul 3638  df-int 4129

This theorem is referenced by:  intnex  4449  intexab  4450  iinexg  4452  onint0  6407  onintrab  6412  onmindif2  6423  fival  7662  elfi2  7664  elfir  7665  dffi2  7673  elfiun  7680  fifo  7682  tz9.1c  7950  tz9.12lem1  7994  tz9.12lem3  7996  rankf  8001  cardf2  8113  cardval3  8122  cardid2  8123  cardcf  8421  cflim2  8432  intwun  8902  wuncval  8909  inttsk  8941  intgru  8981  gruina  8985  mremre  14542  mrcval  14548  asplss  17400  aspsubrg  17402  toponmre  18697  subbascn  18858  insiga  26580  sigagenval  26583  sigagensiga  26584  dmsigagen  26587  dfrtrcl2  27350  dfon2lem8  27603  dfon2lem9  27604  igenval  28861  elrfi  29030  ismrcd1  29034  mzpval  29068  dmmzp  29069  pclvalN  33534