Metamath Proof Explorer

Theorem inxpssres

Description: Intersection with a Cartesian product is a subclass of restriction. (Contributed by Peter Mazsa, 19-Jul-2019)

Ref Expression
Assertion inxpssres 
|- ( R i^i ( A X. B ) ) C_ ( R |` A )

Proof

Step Hyp Ref Expression
1 ssid 
 |-  A C_ A
2 ssv 
 |-  B C_ _V
3 xpss12 
 |-  ( ( A C_ A /\ B C_ _V ) -> ( A X. B ) C_ ( A X. _V ) )
4 1 2 3 mp2an 
 |-  ( A X. B ) C_ ( A X. _V )
5 sslin 
 |-  ( ( A X. B ) C_ ( A X. _V ) -> ( R i^i ( A X. B ) ) C_ ( R i^i ( A X. _V ) ) )
6 4 5 ax-mp 
 |-  ( R i^i ( A X. B ) ) C_ ( R i^i ( A X. _V ) )
7 df-res 
 |-  ( R |` A ) = ( R i^i ( A X. _V ) )
8 6 7 sseqtrri 
 |-  ( R i^i ( A X. B ) ) C_ ( R |` A )