cnvex - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cnvex		Structured version Visualization version GIF version

Theorem cnvex 7971

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∈ wcel 2147 Vcvv 3454 ^◡ccnv 5657

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-ext 2735 ax-sep 5255 ax-pow 5334 ax-pr 5398 ax-un 7783

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-sb 2102 df-clab 2742 df-cleq 2755 df-clel 2839 df-ral 3081 df-rex 3091 df-rab 3417 df-v 3456 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-br 5109 df-opab 5174 df-xp 5664 df-rel 5665 df-cnv 5666 df-dm 5668 df-rn 5669

This theorem is used by: f1oexbi 7974 funcnvuni 7978 cnvf1o 8159 brtpos2 8287 pw2f1o 9139 sbthlem10 9153 fodomr 9185 ssenen 9208 cnfcomlem 9737 infxpenlem 10131 enfin2i 10438 fin1a2lem7 10523 fpwwe 10770 canthwelem 10774 axdc4uzlem 14166 hashfacen 14640 catcisolem 18335 oduleval 18513 gicsubgen 19544 isunit 20654 znle 21897 evpmss 21947 psgnevpmb 21948 ptbasfi 23955 nghmfval 25096 fta1glem2 26542 fta1blem 26544 lgsqrlem4 27733 tocycf 33777 evpmval 33805 altgnsg 33809 elrgspnsubrunlem2 33908 elrspunidl 34082 1arithidom 34173 irngval 34428 locfinreflem 34583 zarcmplem 34624 qqhval 34715 mbfmcnt 35011 derangenlem 36144 mthmval 36548 colinearex 37040 fvline 37124 ptrest 38805 poimir 38839 tendoi2 42118 dihopelvalcpre 42571 pw2f1ocnv 44310 cnvintabd 44864 clcnvlem 44884 frege133 45257 binomcxplemnotnn0 45601 fzisoeu 46589 gricushgr 49288 uspgrlim 49363 tposideq 50332