Theorem cnvxp

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	$$⊢{\left(A\times B\right)}^{-1}=B\times A$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{\left(A\times B\right)}^{-1}$$
2		relxp	$$⊢\mathrm{Rel}\left(B\times A\right)$$
3		vex	$$⊢x\in \mathrm{V}$$
4		vex	$$⊢y\in \mathrm{V}$$
5	3 4	brcnv	$$⊢x{\left(A\times B\right)}^{-1}y\leftrightarrow y\left(A\times B\right)x$$
6		ancom	$$⊢\left(y\in A\wedge x\in B\right)\leftrightarrow \left(x\in B\wedge y\in A\right)$$
7		brxp	$$⊢y\left(A\times B\right)x\leftrightarrow \left(y\in A\wedge x\in B\right)$$
8		brxp	$$⊢x\left(B\times A\right)y\leftrightarrow \left(x\in B\wedge y\in A\right)$$
9	6 7 8	3bitr4i	$$⊢y\left(A\times B\right)x\leftrightarrow x\left(B\times A\right)y$$
10	5 9	bitri	$$⊢x{\left(A\times B\right)}^{-1}y\leftrightarrow x\left(B\times A\right)y$$
11	1 2 10	eqbrriv	$$⊢{\left(A\times B\right)}^{-1}=B\times A$$