Theorem cnvex 7861

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436  ^◡ccnv 5618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-xp 5625  df-rel 5626  df-cnv 5627  df-dm 5629  df-rn 5630

This theorem is referenced by:  f1oexbi  7864  funcnvuni  7868  cnvf1o  8047  brtpos2  8168  pw2f1o  9001  sbthlem10  9015  fodomr  9047  ssenen  9070  cnfcomlem  9595  infxpenlem  9910  enfin2i  10218  fin1a2lem7  10303  fpwwe  10543  canthwelem  10547  axdc4uzlem  13896  hashfacen  14367  catcisolem  18023  oduleval  18201  gicsubgen  19197  isunit  20297  znle  21479  evpmss  21529  psgnevpmb  21530  ptbasfi  23502  nghmfval  24643  fta1glem2  26107  fta1blem  26109  lgsqrlem4  27293  tocycf  33093  evpmval  33121  altgnsg  33125  elrgspnsubrunlem2  33222  elrspunidl  33400  1arithidom  33509  irngval  33705  locfinreflem  33860  zarcmplem  33901  qqhval  33992  mbfmcnt  34288  derangenlem  35222  mthmval  35626  colinearex  36111  fvline  36195  ptrest  37665  poimir  37699  tendoi2  40900  dihopelvalcpre  41353  pw2f1ocnv  43135  cnvintabd  43701  clcnvlem  43721  frege133  44094  binomcxplemnotnn0  44454  fzisoeu  45406  gricushgr  48022  uspgrlim  48097  tposideq  48993