Metamath Proof Explorer


Theorem intmin

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)

Ref Expression
Assertion intmin
|- ( A e. B -> |^| { x e. B | A C_ x } = A )

Proof

Step Hyp Ref Expression
1 vex
 |-  y e. _V
2 1 elintrab
 |-  ( y e. |^| { x e. B | A C_ x } <-> A. x e. B ( A C_ x -> y e. x ) )
3 ssid
 |-  A C_ A
4 sseq2
 |-  ( x = A -> ( A C_ x <-> A C_ A ) )
5 eleq2
 |-  ( x = A -> ( y e. x <-> y e. A ) )
6 4 5 imbi12d
 |-  ( x = A -> ( ( A C_ x -> y e. x ) <-> ( A C_ A -> y e. A ) ) )
7 6 rspcv
 |-  ( A e. B -> ( A. x e. B ( A C_ x -> y e. x ) -> ( A C_ A -> y e. A ) ) )
8 3 7 mpii
 |-  ( A e. B -> ( A. x e. B ( A C_ x -> y e. x ) -> y e. A ) )
9 2 8 syl5bi
 |-  ( A e. B -> ( y e. |^| { x e. B | A C_ x } -> y e. A ) )
10 9 ssrdv
 |-  ( A e. B -> |^| { x e. B | A C_ x } C_ A )
11 ssintub
 |-  A C_ |^| { x e. B | A C_ x }
12 11 a1i
 |-  ( A e. B -> A C_ |^| { x e. B | A C_ x } )
13 10 12 eqssd
 |-  ( A e. B -> |^| { x e. B | A C_ x } = A )