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

Theorem intex 4297
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 3580 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
2 intss1 4007 . . . . 5  |-  ( x  e.  A  ->  |^| A  C_  x )
3 vex 2902 . . . . . 6  |-  x  e. 
_V
43ssex 4288 . . . . 5  |-  ( |^| A  C_  x  ->  |^| A  e.  _V )
52, 4syl 16 . . . 4  |-  ( x  e.  A  ->  |^| A  e.  _V )
65exlimiv 1641 . . 3  |-  ( E. x  x  e.  A  ->  |^| A  e.  _V )
71, 6sylbi 188 . 2  |-  ( A  =/=  (/)  ->  |^| A  e. 
_V )
8 vprc 4282 . . . 4  |-  -.  _V  e.  _V
9 inteq 3995 . . . . . 6  |-  ( A  =  (/)  ->  |^| A  =  |^| (/) )
10 int0 4006 . . . . . 6  |-  |^| (/)  =  _V
119, 10syl6eq 2435 . . . . 5  |-  ( A  =  (/)  ->  |^| A  =  _V )
1211eleq1d 2453 . . . 4  |-  ( A  =  (/)  ->  ( |^| A  e.  _V  <->  _V  e.  _V ) )
138, 12mtbiri 295 . . 3  |-  ( A  =  (/)  ->  -.  |^| A  e.  _V )
1413necon2ai 2595 . 2  |-  ( |^| A  e.  _V  ->  A  =/=  (/) )
157, 14impbii 181 1  |-  ( A  =/=  (/)  <->  |^| A  e.  _V )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   E.wex 1547    = wceq 1649    e. wcel 1717    =/= wne 2550   _Vcvv 2899    C_ wss 3263   (/)c0 3571   |^|cint 3992
This theorem is referenced by:  intnex  4298  intexab  4299  iinexg  4301  onint0  4716  onintrab  4721  onmindif2  4732  fival  7352  elfi2  7354  elfir  7355  dffi2  7363  elfiun  7370  fifo  7372  tz9.1c  7599  tz9.12lem1  7646  tz9.12lem3  7648  rankf  7653  cardf2  7763  cardval3  7772  cardid2  7773  cardcf  8065  cflim2  8076  intwun  8543  wuncval  8550  inttsk  8582  intgru  8622  gruina  8626  mremre  13756  mrcval  13762  asplss  16315  aspsubrg  16317  toponmre  17080  subbascn  17240  insiga  24316  sigagenval  24319  sigagensiga  24320  dmsigagen  24323  dfrtrcl2  24927  dfon2lem8  25170  dfon2lem9  25171  igenval  26362  elrfi  26439  ismrcd1  26443  mzpval  26480  dmmzp  26481  pclvalN  30004
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-v 2901  df-dif 3266  df-in 3270  df-ss 3277  df-nul 3572  df-int 3993
  Copyright terms: Public domain W3C validator