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 6152

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 6104	. 2 ⊢ Rel ^◡(𝐴 × 𝐵)
2		relxp 5677	. 2 ⊢ Rel (𝐵 × 𝐴)
3		vex 3457	. . . 4 ⊢ 𝑥 ∈ V
4		vex 3457	. . . 4 ⊢ 𝑦 ∈ V
5	3, 4	brcnv 5866	. . 3 ⊢ (𝑥^◡(𝐴 × 𝐵)𝑦 ↔ 𝑦(𝐴 × 𝐵)𝑥)
6		ancom 466	. . . 4 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴))
7		brxp 5708	. . . 4 ⊢ (𝑦(𝐴 × 𝐵)𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
8		brxp 5708	. . . 4 ⊢ (𝑥(𝐵 × 𝐴)𝑦 ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴))
9	6, 7, 8	3bitr4i 306	. . 3 ⊢ (𝑦(𝐴 × 𝐵)𝑥 ↔ 𝑥(𝐵 × 𝐴)𝑦)
10	5, 9	bitri 278	. 2 ⊢ (𝑥^◡(𝐴 × 𝐵)𝑦 ↔ 𝑥(𝐵 × 𝐴)𝑦)
11	1, 2, 10	eqbrriv 5775	1 ⊢ ^◡(𝐴 × 𝐵) = (𝐵 × 𝐴)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∧ wa 401 = wceq 1570 ∈ wcel 2145 class class class wbr 5107 × cxp 5657 ^◡ccnv 5658

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 2734 ax-sep 5255 ax-pr 5402

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 2741 df-cleq 2754 df-clel 2837 df-ral 3079 df-rex 3089 df-rab 3415 df-v 3455 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4283 df-if 4486 df-sn 4588 df-pr 4590 df-op 4594 df-br 5108 df-opab 5172 df-xp 5665 df-rel 5666 df-cnv 5667

This theorem is used by: xp0OLD 6154 rnxp 6167 rnxpss 6169 dminxp 6177 imainrect 6178 cnvrescnv 6193 fparlem3 8114 fparlem4 8115 tposfo 8254 tposf 8255 xpider 8791 xpcomf1o 9067 fpwwe2lem12 10654 trclublem 15070 pjdm 21921 tposmap 22680 ordtrest2 23430 ustneism 24451 trust 24456 metustsym 24782 metust 24785 gtiso 33160 padct 33176 gsumhashmul 33494 ordtcnvNEW 34417 ordtrest2NEW 34420 mbfmcst 34757 eulerpartlemt 34869 0rrv 34949 msrf 36108 mthmpps 36148 elrn3 36328 vxp 38998 trclubgNEW 44445 xpexb 45263 tposresxp 49796 tposf1o 49797

W3C validator