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 7931

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∈ wcel 2146 Vcvv 3458 ^◡ccnv 5665

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 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-ext 2738 ax-sep 5262 ax-pow 5341 ax-pr 5409 ax-un 7745

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 2100 df-clab 2745 df-cleq 2758 df-clel 2841 df-ral 3083 df-rex 3093 df-rab 3420 df-v 3460 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-br 5115 df-opab 5179 df-xp 5672 df-rel 5673 df-cnv 5674 df-dm 5676 df-rn 5677

This theorem is used by: f1oexbi 7934 funcnvuni 7938 cnvf1o 8115 brtpos2 8237 pw2f1o 9080 sbthlem10 9094 fodomr 9126 ssenen 9149 cnfcomlem 9678 infxpenlem 10016 enfin2i 10323 fin1a2lem7 10408 fpwwe 10649 canthwelem 10653 axdc4uzlem 14039 hashfacen 14511 catcisolem 18192 oduleval 18370 gicsubgen 19380 isunit 20488 znle 21723 evpmss 21773 psgnevpmb 21774 ptbasfi 23775 nghmfval 24916 fta1glem2 26363 fta1blem 26365 lgsqrlem4 27550 tocycf 33468 evpmval 33496 altgnsg 33500 elrgspnsubrunlem2 33599 elrspunidl 33767 1arithidom 33858 irngval 34106 locfinreflem 34261 zarcmplem 34302 qqhval 34393 mbfmcnt 34690 derangenlem 35684 mthmval 36088 colinearex 36573 fvline 36657 ptrest 38311 poimir 38345 tendoi2 41610 dihopelvalcpre 42063 pw2f1ocnv 43805 cnvintabd 44370 clcnvlem 44390 frege133 44763 binomcxplemnotnn0 45107 fzisoeu 46060 gricushgr 48723 uspgrlim 48798 tposideq 49707