cnvxp - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cnvxp		Structured version Visualization version GIF version

Theorem cnvxp 6142

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 2194. (Revised by SN, 26-Aug-2026.)

**Assertion**
Ref	Expression
cnvxp	⊢ ^◡(𝐴 × 𝐵) = (𝐵 × 𝐴)

Proof of Theorem cnvxp Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relcnv 6094	. 2 ⊢ Rel ^◡(𝐴 × 𝐵)
2		relxp 5665	. 2 ⊢ Rel (𝐵 × 𝐴)
3		vex 3454	. . . 4 ⊢ 𝑥 ∈ V
4		vex 3454	. . . 4 ⊢ 𝑦 ∈ V
5	3, 4	brcnv 5856	. . 3 ⊢ (𝑥^◡(𝐴 × 𝐵)𝑦 ↔ 𝑦(𝐴 × 𝐵)𝑥)
6		ancom 466	. . . 4 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴))
7		brxp 5696	. . . 4 ⊢ (𝑦(𝐴 × 𝐵)𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
8		brxp 5696	. . . 4 ⊢ (𝑥(𝐵 × 𝐴)𝑦 ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴))
9	6, 7, 8	3bitr4i 306	. . 3 ⊢ (𝑦(𝐴 × 𝐵)𝑥 ↔ 𝑥(𝐵 × 𝐴)𝑦)
10	5, 9	bitri 278	. 2 ⊢ (𝑥^◡(𝐴 × 𝐵)𝑦 ↔ 𝑥(𝐵 × 𝐴)𝑦)
11	1, 2, 10	eqbrriv 5763	1 ⊢ ^◡(𝐴 × 𝐵) = (𝐵 × 𝐴)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∧ wa 401 = wceq 1570 ∈ wcel 2145 class class class wbr 5102 × cxp 5645 ^◡ccnv 5646

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-ext 2732 ax-sep 5248 ax-pr 5390

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-sb 2100 df-clab 2739 df-cleq 2752 df-clel 2835 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4279 df-if 4482 df-sn 4584 df-pr 4586 df-op 4590 df-br 5103 df-opab 5167 df-xp 5653 df-rel 5654 df-cnv 5655

This theorem is used by: xp0OLD 6144 rnxp 6157 rnxpss 6159 dminxp 6167 imainrect 6168 cnvrescnv 6183 fparlem3 8108 fparlem4 8109 tposfo 8248 tposf 8249 xpider 8787 xpcomf1o 9063 fpwwe2lem12 10698 trclublem 15115 pjdm 21974 tposmap 22733 ordtrest2 23483 ustneism 24504 trust 24509 metustsym 24835 metust 24838 gtiso 33227 padct 33243 gsumhashmul 33561 ordtcnvNEW 34485 ordtrest2NEW 34488 mbfmcst 34825 eulerpartlemt 34937 0rrv 35017 msrf 36228 mthmpps 36268 elrn3 36448 vxp 39115 trclubgNEW 44562 xpexb 45380 tposresxp 49913 tposf1o 49914

W3C validator