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 7918

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∈ wcel 2143 Vcvv 3455 ^◡ccnv 5660

This proof depends on 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 5257 ax-pow 5336 ax-pr 5404 ax-un 7732

This proof 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 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-br 5110 df-opab 5174 df-xp 5667 df-rel 5668 df-cnv 5669 df-dm 5671 df-rn 5672

This theorem is used by: f1oexbi 7921 funcnvuni 7925 cnvf1o 8102 brtpos2 8224 pw2f1o 9066 sbthlem10 9080 fodomr 9112 ssenen 9135 cnfcomlem 9664 infxpenlem 10002 enfin2i 10309 fin1a2lem7 10394 fpwwe 10635 canthwelem 10639 axdc4uzlem 14024 hashfacen 14496 catcisolem 18171 oduleval 18349 gicsubgen 19353 isunit 20460 znle 21695 evpmss 21745 psgnevpmb 21746 ptbasfi 23747 nghmfval 24888 fta1glem2 26335 fta1blem 26337 lgsqrlem4 27522 tocycf 33446 evpmval 33474 altgnsg 33478 elrgspnsubrunlem2 33577 elrspunidl 33745 1arithidom 33836 irngval 34084 locfinreflem 34239 zarcmplem 34280 qqhval 34371 mbfmcnt 34667 derangenlem 35671 mthmval 36075 colinearex 36560 fvline 36644 ptrest 38298 poimir 38332 tendoi2 41597 dihopelvalcpre 42050 pw2f1ocnv 43792 cnvintabd 44357 clcnvlem 44377 frege133 44750 binomcxplemnotnn0 45094 fzisoeu 46047 gricushgr 48710 uspgrlim 48785 tposideq 49694