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

Theorem cnvex 5211
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  |-  A  e. 
_V
Assertion
Ref Expression
cnvex  |-  `' A  e.  _V

Proof of Theorem cnvex
StepHypRef Expression
1 cnvex.1 . 2  |-  A  e. 
_V
2 cnvexg 5210 . 2  |-  ( A  e.  _V  ->  `' A  e.  _V )
31, 2ax-mp 8 1  |-  `' A  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1686   _Vcvv 2790   `'ccnv 4690
This theorem is referenced by:  funcnvuni  5319  cnvf1o  6219  brtpos2  6242  pw2f1o  6969  sbthlem10  6982  fodomr  7014  ssenen  7037  cantnfdm  7367  cantnfval  7371  cantnff  7377  cnfcomlem  7404  cnfcom2  7407  cnfcom3lem  7408  cnfcom3  7409  infxpenlem  7643  enfin2i  7949  canthwelem  8274  axdc4uzlem  11046  hashfacen  11394  xpscf  13470  xpsfval  13471  xpssca  13482  xpsvsca  13483  catcisolem  13940  oduleval  14237  gicsubgen  14744  isunit  15441  znle  16492  ptbasfi  17278  nghmfval  18233  fta1glem2  19554  fta1blem  19556  lgsqrlem4  20585  mbfmcnt  23575  derangenlem  23704  colinearex  24685  fvline  24769  pw2f1ocnv  27141  tendoi2  31057  dihopelvalcpre  31511
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-xp 4697  df-rel 4698  df-cnv 4699  df-dm 4701  df-rn 4702
  Copyright terms: Public domain W3C validator