Metamath Proof Explorer


Theorem preddif

Description: Difference law for predecessor classes. (Contributed by Scott Fenton, 14-Apr-2011)

Ref Expression
Assertion preddif
|- Pred ( R , ( A \ B ) , X ) = ( Pred ( R , A , X ) \ Pred ( R , B , X ) )

Proof

Step Hyp Ref Expression
1 indifdir
 |-  ( ( A \ B ) i^i ( `' R " { X } ) ) = ( ( A i^i ( `' R " { X } ) ) \ ( B i^i ( `' R " { X } ) ) )
2 df-pred
 |-  Pred ( R , ( A \ B ) , X ) = ( ( A \ 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 difeq12i
 |-  ( Pred ( R , A , X ) \ Pred ( R , B , X ) ) = ( ( A i^i ( `' R " { X } ) ) \ ( B i^i ( `' R " { X } ) ) )
6 1 2 5 3eqtr4i
 |-  Pred ( R , ( A \ B ) , X ) = ( Pred ( R , A , X ) \ Pred ( R , B , X ) )