Description: Distributive law for converse over intersection. Theorem 15 of Suppes p. 62. (Contributed by NM, 25-Mar-1998) (Revised by Mario Carneiro, 26-Jun-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cnvin | |- `' ( A i^i B ) = ( `' A i^i `' B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnvdif | |- `' ( A \ ( A \ B ) ) = ( `' A \ `' ( A \ B ) ) |
|
| 2 | cnvdif | |- `' ( A \ B ) = ( `' A \ `' B ) |
|
| 3 | 2 | difeq2i | |- ( `' A \ `' ( A \ B ) ) = ( `' A \ ( `' A \ `' B ) ) |
| 4 | 1 3 | eqtri | |- `' ( A \ ( A \ B ) ) = ( `' A \ ( `' A \ `' B ) ) |
| 5 | dfin4 | |- ( A i^i B ) = ( A \ ( A \ B ) ) |
|
| 6 | 5 | cnveqi | |- `' ( A i^i B ) = `' ( A \ ( A \ B ) ) |
| 7 | dfin4 | |- ( `' A i^i `' B ) = ( `' A \ ( `' A \ `' B ) ) |
|
| 8 | 4 6 7 | 3eqtr4i | |- `' ( A i^i B ) = ( `' A i^i `' B ) |