Theorem cnvex 7855

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

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

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 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668

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 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-xp 5622  df-rel 5623  df-cnv 5624  df-dm 5626  df-rn 5627

This theorem is referenced by:  f1oexbi  7858  funcnvuni  7862  cnvf1o  8041  brtpos2  8162  pw2f1o  8995  sbthlem10  9009  fodomr  9041  ssenen  9064  cnfcomlem  9589  infxpenlem  9904  enfin2i  10212  fin1a2lem7  10297  fpwwe  10537  canthwelem  10541  axdc4uzlem  13890  hashfacen  14361  catcisolem  18017  oduleval  18195  gicsubgen  19192  isunit  20292  znle  21474  evpmss  21524  psgnevpmb  21525  ptbasfi  23497  nghmfval  24638  fta1glem2  26102  fta1blem  26104  lgsqrlem4  27288  tocycf  33084  evpmval  33112  altgnsg  33116  elrgspnsubrunlem2  33213  elrspunidl  33391  1arithidom  33500  irngval  33696  locfinreflem  33851  zarcmplem  33892  qqhval  33983  mbfmcnt  34279  derangenlem  35213  mthmval  35617  colinearex  36100  fvline  36184  ptrest  37665  poimir  37699  tendoi2  40840  dihopelvalcpre  41293  pw2f1ocnv  43076  cnvintabd  43642  clcnvlem  43662  frege133  44035  binomcxplemnotnn0  44395  fzisoeu  45347  gricushgr  47954  uspgrlim  48029  tposideq  48925