Theorem cnvex 7772

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

Step	Hyp	Ref	Expression
1		cnvex.1	. 2 ⊢ 𝐴 ∈ V
2		cnvexg 7771	. 2 ⊢ (𝐴 ∈ V → ◡𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ ◡𝐴 ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3432  ^◡ccnv 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-xp 5595  df-rel 5596  df-cnv 5597  df-dm 5599  df-rn 5600

This theorem is referenced by:  f1oexbi  7775  funcnvuni  7778  cnvf1o  7951  brtpos2  8048  pw2f1o  8864  sbthlem10  8879  fodomr  8915  ssenen  8938  cnfcomlem  9457  infxpenlem  9769  enfin2i  10077  fin1a2lem7  10162  fpwwe  10402  canthwelem  10406  axdc4uzlem  13703  hashfacen  14166  hashfacenOLD  14167  catcisolem  17825  oduleval  18007  gicsubgen  18894  isunit  19899  znle  20740  evpmss  20791  psgnevpmb  20792  ptbasfi  22732  nghmfval  23886  fta1glem2  25331  fta1blem  25333  lgsqrlem4  26497  tocycf  31384  evpmval  31412  altgnsg  31416  elrspunidl  31606  locfinreflem  31790  zarcmplem  31831  qqhval  31924  mbfmcnt  32235  derangenlem  33133  mthmval  33537  colinearex  34362  fvline  34446  ptrest  35776  poimir  35810  tendoi2  38809  dihopelvalcpre  39262  pw2f1ocnv  40859  cnvintabd  41211  clcnvlem  41231  frege133  41604  binomcxplemnotnn0  41974  fzisoeu  42839  isomushgr  45278  isomgrsym  45288