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 )