Theorem cnvxp 5429

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.

Step	Hyp	Ref	Expression
1		cnvopab 5412	. . 3
2		ancom 450	. . . 4
3	2	opabbii 4516	. . 3
4	1, 3	eqtri 2486	. 2
5		df-xp 5010	. . 3
6	5	cnveqi 5182	. 2
7		df-xp 5010	. 2
8	4, 6, 7	3eqtr4i 2496	1

Syntax hints:  /\wa 369  =wceq 1395  e.wcel 1818  {copab 4509  X.cxp 5002  `'ccnv 5003

This theorem is referenced by:  xp0  5430  rnxp  5442  rnxpss  5444  dminxp  5452  imainrect  5453  fparlem3  6902  fparlem4  6903  tposfo  7001  tposf  7002  xpider  7401  xpcomf1o  7626  fpwwe2lem13  9041  xpsc  14954  pjdm  18738  tposmap  18959  ordtrest2  19705  ustneism  20726  trust  20732  metustsymOLD  21064  metustsym  21065  metustOLD  21070  metust  21071  gtiso  27519  ordtcnvNEW  27902  ordtrest2NEW  27905  mbfmcst  28230  eulerpartlemt  28310  0rrv  28390  msrf  28902  mthmpps  28942  elrn3  29192  xpexb  31363  trclubg  37785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010  df-rel 5011  df-cnv 5012