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

Theorem intssuni 4304
Description: The intersection of a nonempty set is a subclass of its union. (Contributed by NM, 29-Jul-2006.)
Assertion
Ref Expression
intssuni  |-  ( A  =/=  (/)  ->  |^| A  C_  U. A )

Proof of Theorem intssuni
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 r19.2z 3917 . . . 4  |-  ( ( A  =/=  (/)  /\  A. y  e.  A  x  e.  y )  ->  E. y  e.  A  x  e.  y )
21ex 434 . . 3  |-  ( A  =/=  (/)  ->  ( A. y  e.  A  x  e.  y  ->  E. y  e.  A  x  e.  y ) )
3 vex 3116 . . . 4  |-  x  e. 
_V
43elint2 4289 . . 3  |-  ( x  e.  |^| A  <->  A. y  e.  A  x  e.  y )
5 eluni2 4249 . . 3  |-  ( x  e.  U. A  <->  E. y  e.  A  x  e.  y )
62, 4, 53imtr4g 270 . 2  |-  ( A  =/=  (/)  ->  ( x  e.  |^| A  ->  x  e.  U. A ) )
76ssrdv 3510 1  |-  ( A  =/=  (/)  ->  |^| A  C_  U. A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767    =/= wne 2662   A.wral 2814   E.wrex 2815    C_ wss 3476   (/)c0 3785   U.cuni 4245   |^|cint 4282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-v 3115  df-dif 3479  df-in 3483  df-ss 3490  df-nul 3786  df-uni 4246  df-int 4283
This theorem is referenced by:  unissint  4306  intssuni2  4307  fin23lem31  8724  wunint  9094  tskint  9164  incexc  13615  incexc2  13616  subgint  16039  efgval  16550  lbsextlem3  17618  cssmre  18531  uffixfr  20251  uffix2  20252  uffixsn  20253  insiga  27888  dfon2lem8  29075  intidl  30256  elrfi  30457
  Copyright terms: Public domain W3C validator