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 2106  Vcvv 3474  ^◡ccnv 5669

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5293  ax-nul 5300  ax-pow 5357  ax-pr 5421  ax-un 7709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5143  df-opab 5205  df-xp 5676  df-rel 5677  df-cnv 5678  df-dm 5680  df-rn 5681

This theorem is referenced by:  f1oexbi  7903  funcnvuni  7906  cnvf1o  8081  brtpos2  8201  pw2f1o  9062  sbthlem10  9077  fodomr  9113  ssenen  9136  cnfcomlem  9678  infxpenlem  9992  enfin2i  10300  fin1a2lem7  10385  fpwwe  10625  canthwelem  10629  axdc4uzlem  13932  hashfacen  14397  hashfacenOLD  14398  catcisolem  18044  oduleval  18226  gicsubgen  19120  isunit  20141  znle  21023  evpmss  21074  psgnevpmb  21075  ptbasfi  23016  nghmfval  24170  fta1glem2  25615  fta1blem  25617  lgsqrlem4  26781  tocycf  32211  evpmval  32239  altgnsg  32243  elrspunidl  32461  irngval  32651  locfinreflem  32715  zarcmplem  32756  qqhval  32849  mbfmcnt  33162  derangenlem  34057  mthmval  34461  colinearex  34926  fvline  35010  ptrest  36355  poimir  36389  tendoi2  39535  dihopelvalcpre  39988  pw2f1ocnv  41611  cnvintabd  42189  clcnvlem  42209  frege133  42582  binomcxplemnotnn0  42950  fzisoeu  43847  isomushgr  46330  isomgrsym  46340