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

Theorem intex 4324
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 3605 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
2 intss1 4033 . . . . 5  |-  ( x  e.  A  ->  |^| A  C_  x )
3 vex 2927 . . . . . 6  |-  x  e. 
_V
43ssex 4315 . . . . 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 4309 . . . 4  |-  -.  _V  e.  _V
9 inteq 4021 . . . . . 6  |-  ( A  =  (/)  ->  |^| A  =  |^| (/) )
10 int0 4032 . . . . . 6  |-  |^| (/)  =  _V
119, 10syl6eq 2460 . . . . 5  |-  ( A  =  (/)  ->  |^| A  =  _V )
1211eleq1d 2478 . . . 4  |-  ( A  =  (/)  ->  ( |^| A  e.  _V  <->  _V  e.  _V ) )
138, 12mtbiri 295 . . 3  |-  ( A  =  (/)  ->  -.  |^| A  e.  _V )
1413necon2ai 2620 . 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 1721    =/= wne 2575   _Vcvv 2924    C_ wss 3288   (/)c0 3596   |^|cint 4018
This theorem is referenced by:  intnex  4325  intexab  4326  iinexg  4328  onint0  4743  onintrab  4748  onmindif2  4759  fival  7383  elfi2  7385  elfir  7386  dffi2  7394  elfiun  7401  fifo  7403  tz9.1c  7630  tz9.12lem1  7677  tz9.12lem3  7679  rankf  7684  cardf2  7794  cardval3  7803  cardid2  7804  cardcf  8096  cflim2  8107  intwun  8574  wuncval  8581  inttsk  8613  intgru  8653  gruina  8657  mremre  13792  mrcval  13798  asplss  16351  aspsubrg  16353  toponmre  17120  subbascn  17280  insiga  24481  sigagenval  24484  sigagensiga  24485  dmsigagen  24488  dfrtrcl2  25109  dfon2lem8  25368  dfon2lem9  25369  igenval  26569  elrfi  26646  ismrcd1  26650  mzpval  26687  dmmzp  26688  pclvalN  30384
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 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-v 2926  df-dif 3291  df-in 3295  df-ss 3302  df-nul 3597  df-int 4019
  Copyright terms: Public domain W3C validator