Theorem cnvex 7443

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

Syntax hints:   ∈ wcel 2051  Vcvv 3408  ^◡ccnv 5402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2743  ax-sep 5056  ax-nul 5063  ax-pow 5115  ax-pr 5182  ax-un 7277

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-ral 3086  df-rex 3087  df-rab 3090  df-v 3410  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4709  df-br 4926  df-opab 4988  df-xp 5409  df-rel 5410  df-cnv 5411  df-dm 5413  df-rn 5414

This theorem is referenced by:  f1oexbi  7446  funcnvuni  7449  cnvf1o  7612  brtpos2  7699  pw2f1o  8416  sbthlem10  8430  fodomr  8462  ssenen  8485  cnfcomlem  8954  infxpenlem  9231  enfin2i  9539  fin1a2lem7  9624  fpwwe  9864  canthwelem  9868  axdc4uzlem  13164  hashfacen  13623  xpscfcda  16699  xpsfvalcda  16703  xpssca  16719  xpsvsca  16720  catcisolem  17236  oduleval  17611  gicsubgen  18201  isunit  19142  znle  20400  evpmss  20447  psgnevpmb  20448  ptbasfi  21908  nghmfval  23049  fta1glem2  24478  fta1blem  24480  lgsqrlem4  25642  tocycf  30479  altgnsg  30494  locfinreflem  30780  qqhval  30891  mbfmcnt  31203  derangenlem  32040  mthmval  32379  colinearex  33079  fvline  33163  ptrest  34369  poimir  34403  tendoi2  37413  dihopelvalcpre  37866  pw2f1ocnv  39068  cnvintabd  39363  clcnvlem  39384  frege133  39743  binomcxplemnotnn0  40142  fzisoeu  41028  isomushgr  43391  isomgrsym  43401