Metamath Proof Explorer

Theorem ressn

Description: Restriction of a class to a singleton. (Contributed by Mario Carneiro, 28-Dec-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion ressn 
|- ( A |` { B } ) = ( { B } X. ( A " { B } ) )

Proof

Step Hyp Ref Expression
1 relres 
 |-  Rel ( A |` { B } )
2 relxp 
 |-  Rel ( { B } X. ( A " { B } ) )
3 vex 
 |-  x e. _V
4 vex 
 |-  y e. _V
5 3 4 elimasn 
 |-  ( y e. ( A " { x } ) <-> <. x , y >. e. A )
6 elsni 
 |-  ( x e. { B } -> x = B )
7 6 sneqd 
 |-  ( x e. { B } -> { x } = { B } )
8 7 imaeq2d 
 |-  ( x e. { B } -> ( A " { x } ) = ( A " { B } ) )
9 8 eleq2d 
 |-  ( x e. { B } -> ( y e. ( A " { x } ) <-> y e. ( A " { B } ) ) )
10 5 9 bitr3id 
 |-  ( x e. { B } -> ( <. x , y >. e. A <-> y e. ( A " { B } ) ) )
11 10 pm5.32i 
 |-  ( ( x e. { B } /\ <. x , y >. e. A ) <-> ( x e. { B } /\ y e. ( A " { B } ) ) )
12 4 opelresi 
 |-  ( <. x , y >. e. ( A |` { B } ) <-> ( x e. { B } /\ <. x , y >. e. A ) )
13 opelxp 
 |-  ( <. x , y >. e. ( { B } X. ( A " { B } ) ) <-> ( x e. { B } /\ y e. ( A " { B } ) ) )
14 11 12 13 3bitr4i 
 |-  ( <. x , y >. e. ( A |` { B } ) <-> <. x , y >. e. ( { B } X. ( A " { B } ) ) )
15 1 2 14 eqrelriiv 
 |-  ( A |` { B } ) = ( { B } X. ( A " { B } ) )