Theorem cnvex 7912

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 7911	. 2 ⊢ (𝐴 ∈ V → ◡𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ ◡𝐴 ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3474  ^◡ccnv 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-xp 5681  df-rel 5682  df-cnv 5683  df-dm 5685  df-rn 5686

This theorem is referenced by:  f1oexbi  7915  funcnvuni  7918  cnvf1o  8093  brtpos2  8213  pw2f1o  9073  sbthlem10  9088  fodomr  9124  ssenen  9147  cnfcomlem  9690  infxpenlem  10004  enfin2i  10312  fin1a2lem7  10397  fpwwe  10637  canthwelem  10641  axdc4uzlem  13944  hashfacen  14409  hashfacenOLD  14410  catcisolem  18056  oduleval  18238  gicsubgen  19146  isunit  20179  znle  21079  evpmss  21130  psgnevpmb  21131  ptbasfi  23076  nghmfval  24230  fta1glem2  25675  fta1blem  25677  lgsqrlem4  26841  tocycf  32263  evpmval  32291  altgnsg  32295  elrspunidl  32534  irngval  32737  locfinreflem  32808  zarcmplem  32849  qqhval  32942  mbfmcnt  33255  derangenlem  34150  mthmval  34554  colinearex  35020  fvline  35104  ptrest  36475  poimir  36509  tendoi2  39654  dihopelvalcpre  40107  pw2f1ocnv  41761  cnvintabd  42339  clcnvlem  42359  frege133  42732  binomcxplemnotnn0  43100  fzisoeu  43996  isomushgr  46480  isomgrsym  46490