This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrid 
 |-  ( 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 )