Theorem cnvex 7867

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  ^◡ccnv 5623

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-rel 5631  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  f1oexbi  7870  funcnvuni  7874  cnvf1o  8053  brtpos2  8174  pw2f1o  9010  sbthlem10  9024  fodomr  9056  ssenen  9079  cnfcomlem  9608  infxpenlem  9923  enfin2i  10231  fin1a2lem7  10316  fpwwe  10557  canthwelem  10561  axdc4uzlem  13906  hashfacen  14377  catcisolem  18034  oduleval  18212  gicsubgen  19208  isunit  20309  znle  21491  evpmss  21541  psgnevpmb  21542  ptbasfi  23525  nghmfval  24666  fta1glem2  26130  fta1blem  26132  lgsqrlem4  27316  tocycf  33199  evpmval  33227  altgnsg  33231  elrgspnsubrunlem2  33330  elrspunidl  33509  1arithidom  33618  irngval  33842  locfinreflem  33997  zarcmplem  34038  qqhval  34129  mbfmcnt  34425  derangenlem  35365  mthmval  35769  colinearex  36254  fvline  36338  ptrest  37820  poimir  37854  tendoi2  41055  dihopelvalcpre  41508  pw2f1ocnv  43279  cnvintabd  43844  clcnvlem  43864  frege133  44237  binomcxplemnotnn0  44597  fzisoeu  45548  gricushgr  48163  uspgrlim  48238  tposideq  49133