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 ) ) |