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

Theorem intex 4248
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 3540 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
2 intss1 3958 . . . . 5  |-  ( x  e.  A  ->  |^| A  C_  x )
3 vex 2867 . . . . . 6  |-  x  e. 
_V
43ssex 4239 . . . . 5  |-  ( |^| A  C_  x  ->  |^| A  e.  _V )
52, 4syl 15 . . . 4  |-  ( x  e.  A  ->  |^| A  e.  _V )
65exlimiv 1634 . . 3  |-  ( E. x  x  e.  A  ->  |^| A  e.  _V )
71, 6sylbi 187 . 2  |-  ( A  =/=  (/)  ->  |^| A  e. 
_V )
8 vprc 4233 . . . 4  |-  -.  _V  e.  _V
9 inteq 3946 . . . . . 6  |-  ( A  =  (/)  ->  |^| A  =  |^| (/) )
10 int0 3957 . . . . . 6  |-  |^| (/)  =  _V
119, 10syl6eq 2406 . . . . 5  |-  ( A  =  (/)  ->  |^| A  =  _V )
1211eleq1d 2424 . . . 4  |-  ( A  =  (/)  ->  ( |^| A  e.  _V  <->  _V  e.  _V ) )
138, 12mtbiri 294 . . 3  |-  ( A  =  (/)  ->  -.  |^| A  e.  _V )
1413necon2ai 2566 . 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 1541    = wceq 1642    e. wcel 1710    =/= wne 2521   _Vcvv 2864    C_ wss 3228   (/)c0 3531   |^|cint 3943
This theorem is referenced by:  intnex  4249  intexab  4250  iinexg  4252  onint0  4669  onintrab  4674  onmindif2  4685  fival  7256  elfi2  7258  elfir  7259  dffi2  7266  elfiun  7273  fifo  7275  tz9.1c  7502  tz9.12lem1  7549  tz9.12lem3  7551  rankf  7556  cardf2  7666  cardval3  7675  cardid2  7676  cardcf  7968  cflim2  7979  intwun  8447  wuncval  8454  inttsk  8486  intgru  8526  gruina  8530  mremre  13605  mrcval  13611  asplss  16168  aspsubrg  16170  toponmre  16936  subbascn  17090  insiga  23786  sigagenval  23789  sigagensiga  23790  dmsigagen  23793  dfrtrcl2  24449  dfon2lem8  24704  dfon2lem9  24705  igenval  26009  elrfi  26092  ismrcd1  26096  mzpval  26133  dmmzp  26134  pclvalN  30148
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-v 2866  df-dif 3231  df-in 3235  df-ss 3242  df-nul 3532  df-int 3944
  Copyright terms: Public domain W3C validator