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 7938

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∈ wcel 2144 Vcvv 3450 ^◡ccnv 5649

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-ext 2732 ax-sep 5248 ax-pow 5326 ax-pr 5390 ax-un 7752

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-sb 2099 df-clab 2739 df-cleq 2752 df-clel 2835 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-br 5103 df-opab 5167 df-xp 5656 df-rel 5657 df-cnv 5658 df-dm 5660 df-rn 5661

This theorem is used by: f1oexbi 7941 funcnvuni 7945 cnvf1o 8125 brtpos2 8253 pw2f1o 9105 sbthlem10 9119 fodomr 9151 ssenen 9174 cnfcomlem 9704 infxpenlem 10096 enfin2i 10403 fin1a2lem7 10488 fpwwe 10735 canthwelem 10739 axdc4uzlem 14130 hashfacen 14603 catcisolem 18291 oduleval 18469 gicsubgen 19499 isunit 20609 znle 21848 evpmss 21898 psgnevpmb 21899 ptbasfi 23906 nghmfval 25047 fta1glem2 26493 fta1blem 26495 lgsqrlem4 27682 tocycf 33725 evpmval 33753 altgnsg 33757 elrgspnsubrunlem2 33856 elrspunidl 34025 1arithidom 34116 irngval 34364 locfinreflem 34519 zarcmplem 34560 qqhval 34651 mbfmcnt 34947 derangenlem 36023 mthmval 36427 colinearex 36918 fvline 37002 ptrest 38631 poimir 38665 tendoi2 41946 dihopelvalcpre 42399 pw2f1ocnv 44138 cnvintabd 44697 clcnvlem 44717 frege133 45090 binomcxplemnotnn0 45434 fzisoeu 46410 gricushgr 49109 uspgrlim 49184 tposideq 50095