MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  intex Unicode version

Theorem intex 4167
Description: The intersection of a non-empty 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.
StepHypRef Expression
1 n0 3464 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
2 intss1 3877 . . . . 5  |-  ( x  e.  A  ->  |^| A  C_  x )
3 vex 2791 . . . . . 6  |-  x  e. 
_V
43ssex 4158 . . . . 5  |-  ( |^| A  C_  x  ->  |^| A  e.  _V )
52, 4syl 15 . . . 4  |-  ( x  e.  A  ->  |^| A  e.  _V )
65exlimiv 1666 . . 3  |-  ( E. x  x  e.  A  ->  |^| A  e.  _V )
71, 6sylbi 187 . 2  |-  ( A  =/=  (/)  ->  |^| A  e. 
_V )
8 vprc 4152 . . . 4  |-  -.  _V  e.  _V
9 inteq 3865 . . . . . 6  |-  ( A  =  (/)  ->  |^| A  =  |^| (/) )
10 int0 3876 . . . . . 6  |-  |^| (/)  =  _V
119, 10syl6eq 2331 . . . . 5  |-  ( A  =  (/)  ->  |^| A  =  _V )
1211eleq1d 2349 . . . 4  |-  ( A  =  (/)  ->  ( |^| A  e.  _V  <->  _V  e.  _V ) )
138, 12mtbiri 294 . . 3  |-  ( A  =  (/)  ->  -.  |^| A  e.  _V )
1413necon2ai 2491 . 2  |-  ( |^| A  e.  _V  ->  A  =/=  (/) )
157, 14impbii 180 1  |-  ( A  =/=  (/)  <->  |^| A  e.  _V )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   E.wex 1528    = wceq 1623    e. wcel 1684    =/= wne 2446   _Vcvv 2788    C_ wss 3152   (/)c0 3455   |^|cint 3862
This theorem is referenced by:  intnex  4168  intexab  4169  iinexg  4171  onint0  4587  onintrab  4592  onmindif2  4603  fival  7166  elfi2  7168  elfir  7169  dffi2  7176  elfiun  7183  fifo  7185  tz9.1c  7412  tz9.12lem1  7459  tz9.12lem3  7461  rankf  7466  cardf2  7576  cardval3  7585  cardid2  7586  cardcf  7878  cflim2  7889  intwun  8357  wuncval  8364  inttsk  8396  intgru  8436  gruina  8440  mremre  13506  mrcval  13512  asplss  16069  aspsubrg  16071  toponmre  16830  subbascn  16984  insiga  23498  sigagenval  23501  sigagensiga  23502  dmsigagen  23505  dfrtrcl2  24045  dfon2lem8  24146  dfon2lem9  24147  toplat  25290  istopx  25547  prtoptop  25549  indcls2  25996  igenval  26686  elrfi  26769  ismrcd1  26773  mzpval  26810  dmmzp  26811  pclvalN  30079
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-v 2790  df-dif 3155  df-in 3159  df-ss 3166  df-nul 3456  df-int 3863
  Copyright terms: Public domain W3C validator