MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnvex Unicode version

Theorem cnvex 6747
Description: The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 19-Dec-2003.)
Hypothesis
Ref Expression
cnvex.1
Assertion
Ref Expression
cnvex

Proof of Theorem cnvex
StepHypRef Expression
1 cnvex.1 . 2
2 cnvexg 6746 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   cvv 3109  `'ccnv 5003
This theorem is referenced by:  f1oexbi  6750  funcnvuni  6753  cnvf1o  6899  brtpos2  6980  pw2f1o  7642  sbthlem10  7656  fodomr  7688  ssenen  7711  cantnfvalOLD  8138  cnfcomlem  8164  cnfcomlemOLD  8172  cnfcom2OLD  8175  cnfcom3lemOLD  8176  cnfcom3OLD  8177  infxpenlem  8412  enfin2i  8722  canthwelem  9049  axdc4uzlem  12092  hashfacen  12503  xpscf  14963  xpsfval  14964  xpssca  14975  xpsvsca  14976  catcisolem  15433  oduleval  15761  gicsubgen  16326  isunit  17306  znle  18573  evpmss  18622  psgnevpmb  18623  ptbasfi  20082  nghmfval  21229  fta1glem2  22567  fta1blem  22569  lgsqrlem4  23619  locfinreflem  27843  qqhval  27955  mbfmcnt  28239  derangenlem  28615  mthmval  28935  colinearex  29710  fvline  29794  ptrest  30048  pw2f1ocnv  30979  binomcxplemnotnn0  31261  fzisoeu  31500  tendoi2  36521  dihopelvalcpre  36975
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-8 1820  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-pow 4630  ax-pr 4691  ax-un 6592
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-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-xp 5010  df-rel 5011  df-cnv 5012  df-dm 5014  df-rn 5015
  Copyright terms: Public domain W3C validator