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

Metamath Proof Explorer

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 )