Theorem ref5

Description: Two ways to say that an intersection of the identity relation with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 12-Dec-2023)

	Ref	Expression
Assertion	ref5	|- ( ( _I i^i ( A X. B ) ) C_ R <-> A. x e. ( A i^i B ) x R x )

Proof

Step	Hyp	Ref	Expression
1		equcom	|- ( y = x <-> x = y )
2	1	imbi1i	|- ( ( y = x -> x R y ) <-> ( x = y -> x R y ) )
3	2	ralbii	|- ( A. y e. B ( y = x -> x R y ) <-> A. y e. B ( x = y -> x R y ) )
4		breq2	|- ( y = x -> ( x R y <-> x R x ) )
5	4	ceqsralbv	|- ( A. y e. B ( y = x -> x R y ) <-> ( x e. B -> x R x ) )
6	3 5	bitr3i	|- ( A. y e. B ( x = y -> x R y ) <-> ( x e. B -> x R x ) )
7	6	ralbii	|- ( A. x e. A A. y e. B ( x = y -> x R y ) <-> A. x e. A ( x e. B -> x R x ) )
8		idinxpss	|- ( ( _I i^i ( A X. B ) ) C_ R <-> A. x e. A A. y e. B ( x = y -> x R y ) )
9		ralin	|- ( A. x e. ( A i^i B ) x R x <-> A. x e. A ( x e. B -> x R x ) )
10	7 8 9	3bitr4i	|- ( ( _I i^i ( A X. B ) ) C_ R <-> A. x e. ( A i^i B ) x R x )