Theorem cnvex 7923

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  ^◡ccnv 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-xp 5669  df-rel 5670  df-cnv 5671  df-dm 5673  df-rn 5674

This theorem is referenced by:  f1oexbi  7926  funcnvuni  7930  cnvf1o  8107  brtpos2  8229  pw2f1o  9071  sbthlem10  9085  fodomr  9117  ssenen  9140  cnfcomlem  9669  infxpenlem  9998  enfin2i  10306  fin1a2lem7  10391  fpwwe  10632  canthwelem  10636  axdc4uzlem  14021  hashfacen  14493  catcisolem  18168  oduleval  18346  gicsubgen  19350  isunit  20456  znle  21667  evpmss  21717  psgnevpmb  21718  ptbasfi  23719  nghmfval  24860  fta1glem2  26307  fta1blem  26309  lgsqrlem4  27494  tocycf  33418  evpmval  33446  altgnsg  33450  elrgspnsubrunlem2  33549  elrspunidl  33717  1arithidom  33808  irngval  34056  locfinreflem  34211  zarcmplem  34252  qqhval  34343  mbfmcnt  34639  derangenlem  35644  mthmval  36048  colinearex  36533  fvline  36617  ptrest  38251  poimir  38285  tendoi2  41550  dihopelvalcpre  42003  pw2f1ocnv  43747  cnvintabd  44312  clcnvlem  44332  frege133  44705  binomcxplemnotnn0  45049  fzisoeu  46002  gricushgr  48665  uspgrlim  48740  tposideq  49649