Theorem cnvex 7746

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

Syntax hints:   ∈ wcel 2108  Vcvv 3422  ^◡ccnv 5579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-xp 5586  df-rel 5587  df-cnv 5588  df-dm 5590  df-rn 5591

This theorem is referenced by:  f1oexbi  7749  funcnvuni  7752  cnvf1o  7922  brtpos2  8019  pw2f1o  8817  sbthlem10  8832  fodomr  8864  ssenen  8887  cnfcomlem  9387  infxpenlem  9700  enfin2i  10008  fin1a2lem7  10093  fpwwe  10333  canthwelem  10337  axdc4uzlem  13631  hashfacen  14094  hashfacenOLD  14095  catcisolem  17741  oduleval  17923  gicsubgen  18809  isunit  19814  znle  20652  evpmss  20703  psgnevpmb  20704  ptbasfi  22640  nghmfval  23792  fta1glem2  25236  fta1blem  25238  lgsqrlem4  26402  tocycf  31286  evpmval  31314  altgnsg  31318  elrspunidl  31508  locfinreflem  31692  zarcmplem  31733  qqhval  31824  mbfmcnt  32135  derangenlem  33033  mthmval  33437  colinearex  34289  fvline  34373  ptrest  35703  poimir  35737  tendoi2  38736  dihopelvalcpre  39189  pw2f1ocnv  40775  cnvintabd  41100  clcnvlem  41120  frege133  41493  binomcxplemnotnn0  41863  fzisoeu  42729  isomushgr  45166  isomgrsym  45176