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 6158

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∧ wa 401 = wceq 1570 ∈ wcel 2147 class class class wbr 5106 × cxp 5653 ^◡ccnv 5654

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-ext 2735 ax-sep 5252 ax-pr 5395

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 2102 df-clab 2742 df-cleq 2755 df-clel 2839 df-ral 3081 df-rex 3091 df-rab 3417 df-v 3456 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-sn 4589 df-pr 4591 df-op 4839 df-br 5107 df-opab 5171 df-xp 5661 df-rel 5662 df-cnv 5663

This theorem is used by: xp0OLD 6160 rnxp 6173 rnxpss 6175 dminxp 6183 imainrect 6184 cnvrescnv 6199 fparlem3 8149 fparlem4 8150 tposfo 8295 tposf 8296 xpider 8834 xpcomf1o 9110 fpwwe2lem12 10751 trclublem 15174 pjdm 22040 tposmap 22799 ordtrest2 23549 ustneism 24570 trust 24575 metustsym 24901 metust 24904 gtiso 33362 padct 33378 gsumhashmul 33695 ordtcnvNEW 34619 ordtrest2NEW 34622 mbfmcst 34958 eulerpartlemt 35070 0rrv 35150 msrf 36473 mthmpps 36513 elrn3 36704 vxp 39386 trclubgNEW 44808 xpexb 45625 tposresxp 50199 tposf1o 50200

W3C validator