Theorem cnvex 7948

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

Syntax hints:   ∈ wcel 2106  Vcvv 3478  ^◡ccnv 5688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-xp 5695  df-rel 5696  df-cnv 5697  df-dm 5699  df-rn 5700

This theorem is referenced by:  f1oexbi  7951  funcnvuni  7955  cnvf1o  8135  brtpos2  8256  pw2f1o  9116  sbthlem10  9131  fodomr  9167  ssenen  9190  cnfcomlem  9737  infxpenlem  10051  enfin2i  10359  fin1a2lem7  10444  fpwwe  10684  canthwelem  10688  axdc4uzlem  14021  hashfacen  14490  catcisolem  18164  oduleval  18346  gicsubgen  19310  isunit  20390  znle  21569  evpmss  21622  psgnevpmb  21623  ptbasfi  23605  nghmfval  24759  fta1glem2  26223  fta1blem  26225  lgsqrlem4  27408  tocycf  33120  evpmval  33148  altgnsg  33152  elrspunidl  33436  1arithidom  33545  irngval  33700  locfinreflem  33801  zarcmplem  33842  qqhval  33935  mbfmcnt  34250  derangenlem  35156  mthmval  35560  colinearex  36042  fvline  36126  ptrest  37606  poimir  37640  tendoi2  40778  dihopelvalcpre  41231  pw2f1ocnv  43026  cnvintabd  43593  clcnvlem  43613  frege133  43986  binomcxplemnotnn0  44352  fzisoeu  45251  gricushgr  47824  uspgrlim  47895