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

Theorem intmin 3898
Description: Any member of a class is the smallest of those members that include it. (Contributed by NM, 13-Aug-2002.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
Assertion
Ref Expression
intmin  |-  ( A  e.  B  ->  |^| { x  e.  B  |  A  C_  x }  =  A )
Distinct variable groups:    x, A    x, B

Proof of Theorem intmin
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 vex 2804 . . . . 5  |-  y  e. 
_V
21elintrab 3890 . . . 4  |-  ( y  e.  |^| { x  e.  B  |  A  C_  x }  <->  A. x  e.  B  ( A  C_  x  -> 
y  e.  x ) )
3 ssid 3210 . . . . 5  |-  A  C_  A
4 sseq2 3213 . . . . . . 7  |-  ( x  =  A  ->  ( A  C_  x  <->  A  C_  A
) )
5 eleq2 2357 . . . . . . 7  |-  ( x  =  A  ->  (
y  e.  x  <->  y  e.  A ) )
64, 5imbi12d 311 . . . . . 6  |-  ( x  =  A  ->  (
( A  C_  x  ->  y  e.  x )  <-> 
( A  C_  A  ->  y  e.  A ) ) )
76rspcv 2893 . . . . 5  |-  ( A  e.  B  ->  ( A. x  e.  B  ( A  C_  x  -> 
y  e.  x )  ->  ( A  C_  A  ->  y  e.  A
) ) )
83, 7mpii 39 . . . 4  |-  ( A  e.  B  ->  ( A. x  e.  B  ( A  C_  x  -> 
y  e.  x )  ->  y  e.  A
) )
92, 8syl5bi 208 . . 3  |-  ( A  e.  B  ->  (
y  e.  |^| { x  e.  B  |  A  C_  x }  ->  y  e.  A ) )
109ssrdv 3198 . 2  |-  ( A  e.  B  ->  |^| { x  e.  B  |  A  C_  x }  C_  A
)
11 ssintub 3896 . . 3  |-  A  C_  |^|
{ x  e.  B  |  A  C_  x }
1211a1i 10 . 2  |-  ( A  e.  B  ->  A  C_ 
|^| { x  e.  B  |  A  C_  x }
)
1310, 12eqssd 3209 1  |-  ( A  e.  B  ->  |^| { x  e.  B  |  A  C_  x }  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696   A.wral 2556   {crab 2560    C_ wss 3165   |^|cint 3878
This theorem is referenced by:  intmin2  3905  ordintdif  4457  bm2.5ii  4613  onsucmin  4628  rankonidlem  7516  rankval4  7555  mrcid  13531  lspid  15755  aspid  16086  cldcls  16795  spanid  21942  chsupid  22007  igenidl2  26793  pclidN  30707  diaocN  31937
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rab 2565  df-v 2803  df-in 3172  df-ss 3179  df-int 3879
  Copyright terms: Public domain W3C validator