Theorem predin

Description: Intersection law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011)

	Ref	Expression
Assertion	predin	|- Pred ( R , ( A i^i B ) , X ) = ( Pred ( R , A , X ) i^i Pred ( R , B , X ) )

Proof

Step	Hyp	Ref	Expression
1		inindir	|- ( ( A i^i B ) i^i ( `' R " { X } ) ) = ( ( A i^i ( `' R " { X } ) ) i^i ( B i^i ( `' R " { X } ) ) )
2		df-pred	|- Pred ( R , ( A i^i B ) , X ) = ( ( A i^i B ) i^i ( `' R " { X } ) )
3		df-pred	|- Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )
4		df-pred	|- Pred ( R , B , X ) = ( B i^i ( `' R " { X } ) )
5	3 4	ineq12i	|- ( Pred ( R , A , X ) i^i Pred ( R , B , X ) ) = ( ( A i^i ( `' R " { X } ) ) i^i ( B i^i ( `' R " { X } ) ) )
6	1 2 5	3eqtr4i	|- Pred ( R , ( A i^i B ) , X ) = ( Pred ( R , A , X ) i^i Pred ( R , B , X ) )