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

Theorem cnvex 7198
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 𝐴 ∈ V
Assertion
Ref Expression
cnvex 𝐴 ∈ V

Proof of Theorem cnvex
StepHypRef Expression
1 cnvex.1 . 2 𝐴 ∈ V
2 cnvexg 7197 . 2 (𝐴 ∈ V → 𝐴 ∈ V)
31, 2ax-mp 5 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2071  Vcvv 3272  ccnv 5185
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1818  ax-5 1920  ax-6 1986  ax-7 2022  ax-8 2073  ax-9 2080  ax-10 2100  ax-11 2115  ax-12 2128  ax-13 2323  ax-ext 2672  ax-sep 4857  ax-nul 4865  ax-pow 4916  ax-pr 4979  ax-un 7034
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1567  df-ex 1786  df-nf 1791  df-sb 1979  df-eu 2543  df-mo 2544  df-clab 2679  df-cleq 2685  df-clel 2688  df-nfc 2823  df-ral 2987  df-rex 2988  df-rab 2991  df-v 3274  df-dif 3651  df-un 3653  df-in 3655  df-ss 3662  df-nul 3992  df-if 4163  df-pw 4236  df-sn 4254  df-pr 4256  df-op 4260  df-uni 4513  df-br 4729  df-opab 4789  df-xp 5192  df-rel 5193  df-cnv 5194  df-dm 5196  df-rn 5197
This theorem is referenced by:  f1oexbi  7201  funcnvuni  7204  cnvf1o  7364  brtpos2  7446  pw2f1o  8149  sbthlem10  8163  fodomr  8195  ssenen  8218  cnfcomlem  8677  infxpenlem  8917  enfin2i  9224  fin1a2lem7  9309  fpwwe  9549  canthwelem  9553  axdc4uzlem  12865  hashfacen  13319  xpscf  16317  xpsfval  16318  xpssca  16329  xpsvsca  16330  catcisolem  16846  oduleval  17221  gicsubgen  17810  isunit  18746  znle  19975  evpmss  20023  psgnevpmb  20024  ptbasfi  21475  nghmfval  22616  fta1glem2  24014  fta1blem  24016  lgsqrlem4  25162  locfinreflem  30105  qqhval  30216  mbfmcnt  30528  derangenlem  31349  mthmval  31668  colinearex  32362  fvline  32446  ptrest  33608  poimir  33642  tendoi2  36470  dihopelvalcpre  36924  pw2f1ocnv  37991  cnvintabd  38296  clcnvlem  38317  frege133  38677  binomcxplemnotnn0  38942  fzisoeu  39898
  Copyright terms: Public domain W3C validator