Metamath Proof Explorer


Theorem idinxpssinxp3

Description: Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product. (Contributed by Peter Mazsa, 16-Mar-2019) (Proof modification is discouraged.)

Ref Expression
Assertion idinxpssinxp3 I A × A R A × A I A R

Proof

Step Hyp Ref Expression
1 idinxpssinxp2 I A × A R A × A x A x R x
2 idrefALT I A R x A x R x
3 1 2 bitr4i I A × A R A × A I A R