Theorem cnvex 7703

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

Syntax hints:   ∈ wcel 2110  Vcvv 3408  ^◡ccnv 5550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-xp 5557  df-rel 5558  df-cnv 5559  df-dm 5561  df-rn 5562

This theorem is referenced by:  f1oexbi  7706  funcnvuni  7709  cnvf1o  7879  brtpos2  7974  pw2f1o  8750  sbthlem10  8765  fodomr  8797  ssenen  8820  cnfcomlem  9314  infxpenlem  9627  enfin2i  9935  fin1a2lem7  10020  fpwwe  10260  canthwelem  10264  axdc4uzlem  13556  hashfacen  14018  hashfacenOLD  14019  catcisolem  17616  oduleval  17797  gicsubgen  18682  isunit  19675  znle  20501  evpmss  20548  psgnevpmb  20549  ptbasfi  22478  nghmfval  23620  fta1glem2  25064  fta1blem  25066  lgsqrlem4  26230  tocycf  31103  evpmval  31131  altgnsg  31135  elrspunidl  31320  locfinreflem  31504  zarcmplem  31545  qqhval  31636  mbfmcnt  31947  derangenlem  32846  mthmval  33250  colinearex  34099  fvline  34183  ptrest  35513  poimir  35547  tendoi2  38546  dihopelvalcpre  38999  pw2f1ocnv  40562  cnvintabd  40887  clcnvlem  40907  frege133  41281  binomcxplemnotnn0  41647  fzisoeu  42512  isomushgr  44951  isomgrsym  44961