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

Metamath Proof Explorer

Theorem seinxp

Description: Intersection of set-like relation with Cartesian product of its field. (Contributed by Mario Carneiro, 22-Jun-2015)

Ref Expression
Assertion seinxp 
|- ( R Se A <-> ( R i^i ( A X. A ) ) Se A )

Proof

Step Hyp Ref Expression
1 brinxp 
 |-  ( ( y e. A /\ x e. A ) -> ( y R x <-> y ( R i^i ( A X. A ) ) x ) )
2 1 ancoms 
 |-  ( ( x e. A /\ y e. A ) -> ( y R x <-> y ( R i^i ( A X. A ) ) x ) )
3 2 rabbidva 
 |-  ( x e. A -> { y e. A | y R x } = { y e. A | y ( R i^i ( A X. A ) ) x } )
4 3 eleq1d 
 |-  ( x e. A -> ( { y e. A | y R x } e. _V <-> { y e. A | y ( R i^i ( A X. A ) ) x } e. _V ) )
5 4 ralbiia 
 |-  ( A. x e. A { y e. A | y R x } e. _V <-> A. x e. A { y e. A | y ( R i^i ( A X. A ) ) x } e. _V )
6 df-se 
 |-  ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
7 df-se 
 |-  ( ( R i^i ( A X. A ) ) Se A <-> A. x e. A { y e. A | y ( R i^i ( A X. A ) ) x } e. _V )
8 5 6 7 3bitr4i 
 |-  ( R Se A <-> ( R i^i ( A X. A ) ) Se A )