Theorem cnvex 7930

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

Syntax hints:   ∈ wcel 2107  Vcvv 3464  ^◡ccnv 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5278  ax-nul 5288  ax-pow 5347  ax-pr 5414  ax-un 7738

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-nul 4316  df-if 4508  df-pw 4584  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-br 5126  df-opab 5188  df-xp 5673  df-rel 5674  df-cnv 5675  df-dm 5677  df-rn 5678

This theorem is referenced by:  f1oexbi  7933  funcnvuni  7937  cnvf1o  8119  brtpos2  8240  pw2f1o  9100  sbthlem10  9115  fodomr  9151  ssenen  9174  cnfcomlem  9722  infxpenlem  10036  enfin2i  10344  fin1a2lem7  10429  fpwwe  10669  canthwelem  10673  axdc4uzlem  14007  hashfacen  14476  catcisolem  18131  oduleval  18309  gicsubgen  19271  isunit  20346  znle  21518  evpmss  21571  psgnevpmb  21572  ptbasfi  23554  nghmfval  24698  fta1glem2  26163  fta1blem  26165  lgsqrlem4  27348  tocycf  33083  evpmval  33111  altgnsg  33115  elrgspnsubrunlem2  33198  elrspunidl  33397  1arithidom  33506  irngval  33676  locfinreflem  33780  zarcmplem  33821  qqhval  33914  mbfmcnt  34211  derangenlem  35117  mthmval  35521  colinearex  36002  fvline  36086  ptrest  37567  poimir  37601  tendoi2  40738  dihopelvalcpre  41191  pw2f1ocnv  42994  cnvintabd  43561  clcnvlem  43581  frege133  43954  binomcxplemnotnn0  44320  fzisoeu  45257  gricushgr  47832  uspgrlim  47905  tposideq  48735