Description: Commutative law for intersection of classes. Exercise 7 of TakeutiZaring p. 17. (Contributed by NM, 21-Jun-1993) (Proof shortened by SN, 12-Dec-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | incom | |- ( A i^i B ) = ( B i^i A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rabswap | |- { x e. A | x e. B } = { x e. B | x e. A } |
|
| 2 | dfin5 | |- ( A i^i B ) = { x e. A | x e. B } |
|
| 3 | dfin5 | |- ( B i^i A ) = { x e. B | x e. A } |
|
| 4 | 1 2 3 | 3eqtr4i | |- ( A i^i B ) = ( B i^i A ) |