Theorem cnvex 7872

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

Syntax hints:   ∈ wcel 2119  Vcvv 3432  ^◡ccnv 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-xp 5631  df-rel 5632  df-cnv 5633  df-dm 5635  df-rn 5636

This theorem is referenced by:  f1oexbi  7875  funcnvuni  7879  cnvf1o  8057  brtpos2  8179  pw2f1o  9017  sbthlem10  9031  fodomr  9063  ssenen  9086  cnfcomlem  9618  infxpenlem  9933  enfin2i  10241  fin1a2lem7  10326  fpwwe  10567  canthwelem  10571  axdc4uzlem  13943  hashfacen  14414  catcisolem  18075  oduleval  18253  gicsubgen  19252  isunit  20351  znle  21518  evpmss  21568  psgnevpmb  21569  ptbasfi  23571  nghmfval  24712  fta1glem2  26159  fta1blem  26161  lgsqrlem4  27337  tocycf  33205  evpmval  33233  altgnsg  33237  elrgspnsubrunlem2  33336  elrspunidl  33518  1arithidom  33627  irngval  33876  locfinreflem  34031  zarcmplem  34072  qqhval  34163  mbfmcnt  34459  derangenlem  35406  mthmval  35810  colinearex  36295  fvline  36379  ptrest  37993  poimir  38027  tendoi2  41294  dihopelvalcpre  41747  pw2f1ocnv  43489  cnvintabd  44054  clcnvlem  44074  frege133  44447  binomcxplemnotnn0  44807  fzisoeu  45755  gricushgr  48415  uspgrlim  48490  tposideq  49385