Theorem intex 4521

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 3721	. . 3 |- ( A =/= (/) <-> E. x x e. A )
2		intss1 4214	. . . . 5 |- ( x e. A -> |^| A C_ x )
3		vex 3037	. . . . . 6 |- x e. _V
4	3	ssex 4509	. . . . 5 |- ( |^| A C_ x -> |^| A e. _V )
5	2, 4	syl 16	. . . 4 |- ( x e. A -> |^| A e. _V )
6	5	exlimiv 1730	. . 3 |- ( E. x x e. A -> |^| A e. _V )
7	1, 6	sylbi 195	. 2 |- ( A =/= (/) -> |^| A e. _V )
8		vprc 4503	. . . 4 |- -. _V e. _V
9		inteq 4202	. . . . . 6 |- ( A = (/) -> |^| A = |^| (/) )
10		int0 4213	. . . . . 6 |- |^| (/) = _V
11	9, 10	syl6eq 2439	. . . . 5 |- ( A = (/) -> |^| A = _V )
12	11	eleq1d 2451	. . . 4 |- ( A = (/) -> ( |^| A e. _V <-> _V e. _V ) )
13	8, 12	mtbiri 301	. . 3 |- ( A = (/) -> -. |^| A e. _V )
14	13	necon2ai 2617	. 2 |- ( |^| A e. _V -> A =/= (/) )
15	7, 14	impbii 188	1 |- ( A =/= (/) <-> |^| A e. _V )

Syntax hints:   <-> wb 184   = wceq 1399   E.wex 1620   e. wcel 1826   =/= wne 2577   _Vcvv 3034   C_ wss 3389   (/)c0 3711   |^|cint 4199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-v 3036  df-dif 3392  df-in 3396  df-ss 3403  df-nul 3712  df-int 4200

This theorem is referenced by:  intnex  4522  intexab  4523  iinexg  4525  onint0  6530  onintrab  6535  onmindif2  6546  fival  7787  elfi2  7789  elfir  7790  dffi2  7798  elfiun  7805  fifo  7807  tz9.1c  8074  tz9.12lem1  8118  tz9.12lem3  8120  rankf  8125  cardf2  8237  cardval3  8246  cardid2  8247  cardcf  8545  cflim2  8556  intwun  9024  wuncval  9031  inttsk  9063  intgru  9103  gruina  9107  dfrtrcl2  12897  mremre  15011  mrcval  15017  asplss  18091  aspsubrg  18093  toponmre  19680  subbascn  19841  insiga  28286  sigagenval  28289  sigagensiga  28290  dmsigagen  28293  dfon2lem8  29387  dfon2lem9  29388  igenval  30624  elrfi  30792  ismrcd1  30796  mzpval  30830  dmmzp  30831  pclvalN  36027