Theorem cnvex 7865

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

Syntax hints:   ∈ wcel 2109  Vcvv 3438  ^◡ccnv 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-xp 5629  df-rel 5630  df-cnv 5631  df-dm 5633  df-rn 5634

This theorem is referenced by:  f1oexbi  7868  funcnvuni  7872  cnvf1o  8051  brtpos2  8172  pw2f1o  9006  sbthlem10  9020  fodomr  9052  ssenen  9075  cnfcomlem  9614  infxpenlem  9926  enfin2i  10234  fin1a2lem7  10319  fpwwe  10559  canthwelem  10563  axdc4uzlem  13908  hashfacen  14379  catcisolem  18035  oduleval  18213  gicsubgen  19176  isunit  20276  znle  21461  evpmss  21511  psgnevpmb  21512  ptbasfi  23484  nghmfval  24626  fta1glem2  26090  fta1blem  26092  lgsqrlem4  27276  tocycf  33072  evpmval  33100  altgnsg  33104  elrgspnsubrunlem2  33201  elrspunidl  33378  1arithidom  33487  irngval  33659  locfinreflem  33809  zarcmplem  33850  qqhval  33941  mbfmcnt  34238  derangenlem  35146  mthmval  35550  colinearex  36036  fvline  36120  ptrest  37601  poimir  37635  tendoi2  40777  dihopelvalcpre  41230  pw2f1ocnv  43013  cnvintabd  43579  clcnvlem  43599  frege133  43972  binomcxplemnotnn0  44332  fzisoeu  45285  gricushgr  47905  uspgrlim  47980  tposideq  48876