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

Theorem cnvxp 5707
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 5689 . . 3 {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑦𝐴𝑥𝐵)}
2 ancom 465 . . . 4 ((𝑦𝐴𝑥𝐵) ↔ (𝑥𝐵𝑦𝐴))
32opabbii 4867 . . 3 {⟨𝑥, 𝑦⟩ ∣ (𝑦𝐴𝑥𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐴)}
41, 3eqtri 2780 . 2 {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐴)}
5 df-xp 5270 . . 3 (𝐴 × 𝐵) = {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)}
65cnveqi 5450 . 2 (𝐴 × 𝐵) = {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)}
7 df-xp 5270 . 2 (𝐵 × 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐴)}
84, 6, 73eqtr4i 2790 1 (𝐴 × 𝐵) = (𝐵 × 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1630  wcel 2137  {copab 4862   × cxp 5262  ccnv 5263
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pr 5053
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-rab 3057  df-v 3340  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-sn 4320  df-pr 4322  df-op 4326  df-br 4803  df-opab 4863  df-xp 5270  df-rel 5271  df-cnv 5272
This theorem is referenced by:  xp0  5708  rnxp  5720  rnxpss  5722  dminxp  5730  imainrect  5731  fparlem3  7445  fparlem4  7446  tposfo  7546  tposf  7547  xpider  7983  xpcomf1o  8212  fpwwe2lem13  9654  trclublem  13933  xpsc  16417  pjdm  20251  tposmap  20463  ordtrest2  21208  ustneism  22226  trust  22232  metustsym  22559  metust  22562  gtiso  29785  padct  29804  ordtcnvNEW  30273  ordtrest2NEW  30276  mbfmcst  30628  eulerpartlemt  30740  0rrv  30820  msrf  31744  mthmpps  31784  elrn3  31957  trclubgNEW  38425  xpexb  39158
  Copyright terms: Public domain W3C validator