Description: The converse of a Cartesian product. Exercise 11 of Suppes p. 67. (Contributed by NM, 14-Aug-1999) (Proof shortened by Andrew Salmon, 27-Aug-2011) Avoid ax-11 . (Revised by SN, 26-Aug-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cnvxp | |- `' ( A X. B ) = ( B X. A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | relcnv | |- Rel `' ( A X. B ) |
|
| 2 | relxp | |- Rel ( B X. A ) |
|
| 3 | vex | |- x e. _V |
|
| 4 | vex | |- y e. _V |
|
| 5 | 3 4 | brcnv | |- ( x `' ( A X. B ) y <-> y ( A X. B ) x ) |
| 6 | ancom | |- ( ( y e. A /\ x e. B ) <-> ( x e. B /\ y e. A ) ) |
|
| 7 | brxp | |- ( y ( A X. B ) x <-> ( y e. A /\ x e. B ) ) |
|
| 8 | brxp | |- ( x ( B X. A ) y <-> ( x e. B /\ y e. A ) ) |
|
| 9 | 6 7 8 | 3bitr4i | |- ( y ( A X. B ) x <-> x ( B X. A ) y ) |
| 10 | 5 9 | bitri | |- ( x `' ( A X. B ) y <-> x ( B X. A ) y ) |
| 11 | 1 2 10 | eqbrriv | |- `' ( A X. B ) = ( B X. A ) |