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 6146

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 2193. (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 6099	. 2 ⊢ Rel ^◡(𝐴 × 𝐵)
2		relxp 5668	. 2 ⊢ Rel (𝐵 × 𝐴)
3		vex 3454	. . . 4 ⊢ 𝑥 ∈ V
4		vex 3454	. . . 4 ⊢ 𝑦 ∈ V
5	3, 4	brcnv 5859	. . 3 ⊢ (𝑥^◡(𝐴 × 𝐵)𝑦 ↔ 𝑦(𝐴 × 𝐵)𝑥)
6		ancom 466	. . . 4 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴))
7		brxp 5699	. . . 4 ⊢ (𝑦(𝐴 × 𝐵)𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
8		brxp 5699	. . . 4 ⊢ (𝑥(𝐵 × 𝐴)𝑦 ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴))
9	6, 7, 8	3bitr4i 306	. . 3 ⊢ (𝑦(𝐴 × 𝐵)𝑥 ↔ 𝑥(𝐵 × 𝐴)𝑦)
10	5, 9	bitri 278	. 2 ⊢ (𝑥^◡(𝐴 × 𝐵)𝑦 ↔ 𝑥(𝐵 × 𝐴)𝑦)
11	1, 2, 10	eqbrriv 5766	1 ⊢ ^◡(𝐴 × 𝐵) = (𝐵 × 𝐴)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∧ wa 401 = wceq 1569 ∈ wcel 2144 class class class wbr 5102 × cxp 5648 ^◡ccnv 5649

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 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 1572 df-fal 1582 df-ex 1812 df-sb 2099 df-clab 2739 df-cleq 2752 df-clel 2835 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-sn 4584 df-pr 4586 df-op 4590 df-br 5103 df-opab 5167 df-xp 5656 df-rel 5657 df-cnv 5658

This theorem is used by: xp0OLD 6148 rnxp 6161 rnxpss 6163 dminxp 6171 imainrect 6172 cnvrescnv 6187 fparlem3 8125 fparlem4 8126 tposfo 8270 tposf 8271 xpider 8809 xpcomf1o 9085 fpwwe2lem12 10727 trclublem 15148 pjdm 22013 tposmap 22772 ordtrest2 23522 ustneism 24543 trust 24548 metustsym 24874 metust 24877 gtiso 33294 padct 33310 gsumhashmul 33628 ordtcnvNEW 34552 ordtrest2NEW 34555 mbfmcst 34891 eulerpartlemt 35003 0rrv 35083 msrf 36307 mthmpps 36347 elrn3 36527 vxp 39196 trclubgNEW 44618 xpexb 45436 tposresxp 49991 tposf1o 49992

W3C validator