Theorem cnvex 7900

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453  ^◡ccnv 5642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pow 5319  ax-pr 5387  ax-un 7712

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-xp 5649  df-rel 5650  df-cnv 5651  df-dm 5653  df-rn 5654

This theorem is referenced by:  f1oexbi  7903  funcnvuni  7907  cnvf1o  8083  brtpos2  8205  pw2f1o  9047  sbthlem10  9061  fodomr  9093  ssenen  9116  cnfcomlem  9647  infxpenlem  9962  enfin2i  10271  fin1a2lem7  10356  fpwwe  10597  canthwelem  10601  axdc4uzlem  13989  hashfacen  14460  catcisolem  18133  oduleval  18311  gicsubgen  19309  isunit  20408  znle  21575  evpmss  21625  psgnevpmb  21626  ptbasfi  23628  nghmfval  24769  fta1glem2  26216  fta1blem  26218  lgsqrlem4  27400  tocycf  33257  evpmval  33285  altgnsg  33289  elrgspnsubrunlem2  33389  elrspunidl  33574  1arithidom  33693  irngval  33942  locfinreflem  34097  zarcmplem  34138  qqhval  34229  mbfmcnt  34525  derangenlem  35481  mthmval  35885  colinearex  36370  fvline  36454  ptrest  38078  poimir  38112  tendoi2  41379  dihopelvalcpre  41832  pw2f1ocnv  43574  cnvintabd  44139  clcnvlem  44159  frege133  44532  binomcxplemnotnn0  44892  fzisoeu  45839  gricushgr  48499  uspgrlim  48574  tposideq  49469