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