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

Theorem cnvxp 6157
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.)
Assertion
Ref Expression
cnvxp (𝐴 × 𝐵) = (𝐵 × 𝐴)

Proof of Theorem cnvxp
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnvopab 6139 . . 3 {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑦𝐴𝑥𝐵)}
2 ancom 462 . . . 4 ((𝑦𝐴𝑥𝐵) ↔ (𝑥𝐵𝑦𝐴))
32opabbii 5216 . . 3 {⟨𝑥, 𝑦⟩ ∣ (𝑦𝐴𝑥𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐴)}
41, 3eqtri 2761 . 2 {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐴)}
5 df-xp 5683 . . 3 (𝐴 × 𝐵) = {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)}
65cnveqi 5875 . 2 (𝐴 × 𝐵) = {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)}
7 df-xp 5683 . 2 (𝐵 × 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐴)}
84, 6, 73eqtr4i 2771 1 (𝐴 × 𝐵) = (𝐵 × 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 397   = wceq 1542  wcel 2107  {copab 5211   × cxp 5675  ccnv 5676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-rel 5684  df-cnv 5685
This theorem is referenced by:  xp0  6158  rnxp  6170  rnxpss  6172  dminxp  6180  imainrect  6181  cnvrescnv  6195  fparlem3  8100  fparlem4  8101  tposfo  8238  tposf  8239  xpider  8782  xpcomf1o  9061  fpwwe2lem12  10637  trclublem  14942  pjdm  21262  tposmap  21959  ordtrest2  22708  ustneism  23728  trust  23734  metustsym  24064  metust  24067  gtiso  31922  padct  31944  gsumhashmul  32208  ordtcnvNEW  32900  ordtrest2NEW  32903  mbfmcst  33258  eulerpartlemt  33370  0rrv  33450  msrf  34533  mthmpps  34573  elrn3  34732  trclubgNEW  42369  xpexb  43213
  Copyright terms: Public domain W3C validator