Theorem cnvex 7901

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447  ^◡ccnv 5637

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-cnv 5646  df-dm 5648  df-rn 5649

This theorem is referenced by:  f1oexbi  7904  funcnvuni  7908  cnvf1o  8090  brtpos2  8211  pw2f1o  9046  sbthlem10  9060  fodomr  9092  ssenen  9115  cnfcomlem  9652  infxpenlem  9966  enfin2i  10274  fin1a2lem7  10359  fpwwe  10599  canthwelem  10603  axdc4uzlem  13948  hashfacen  14419  catcisolem  18072  oduleval  18250  gicsubgen  19211  isunit  20282  znle  21446  evpmss  21495  psgnevpmb  21496  ptbasfi  23468  nghmfval  24610  fta1glem2  26074  fta1blem  26076  lgsqrlem4  27260  tocycf  33074  evpmval  33102  altgnsg  33106  elrgspnsubrunlem2  33199  elrspunidl  33399  1arithidom  33508  irngval  33680  locfinreflem  33830  zarcmplem  33871  qqhval  33962  mbfmcnt  34259  derangenlem  35158  mthmval  35562  colinearex  36048  fvline  36132  ptrest  37613  poimir  37647  tendoi2  40789  dihopelvalcpre  41242  pw2f1ocnv  43026  cnvintabd  43592  clcnvlem  43612  frege133  43985  binomcxplemnotnn0  44345  fzisoeu  45298  gricushgr  47917  uspgrlim  47991  tposideq  48876