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 7926

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∈ wcel 2145 Vcvv 3453 ^◡ccnv 5658

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 2147 ax-9 2155 ax-ext 2734 ax-sep 5255 ax-pow 5334 ax-pr 5402 ax-un 7740

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 2741 df-cleq 2754 df-clel 2837 df-ral 3079 df-rex 3089 df-rab 3415 df-v 3455 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-br 5108 df-opab 5172 df-xp 5665 df-rel 5666 df-cnv 5667 df-dm 5669 df-rn 5670

This theorem is used by: f1oexbi 7929 funcnvuni 7933 cnvf1o 8112 brtpos2 8234 pw2f1o 9084 sbthlem10 9098 fodomr 9130 ssenen 9153 cnfcomlem 9682 infxpenlem 10020 enfin2i 10327 fin1a2lem7 10412 fpwwe 10659 canthwelem 10663 axdc4uzlem 14051 hashfacen 14523 catcisolem 18205 oduleval 18383 gicsubgen 19412 isunit 20520 znle 21755 evpmss 21805 psgnevpmb 21806 ptbasfi 23813 nghmfval 24954 fta1glem2 26401 fta1blem 26403 lgsqrlem4 27593 tocycf 33565 evpmval 33593 altgnsg 33597 elrgspnsubrunlem2 33696 elrspunidl 33864 1arithidom 33955 irngval 34203 locfinreflem 34358 zarcmplem 34399 qqhval 34490 mbfmcnt 34787 derangenlem 35758 mthmval 36162 colinearex 36648 fvline 36732 ptrest 38376 poimir 38410 tendoi2 41676 dihopelvalcpre 42129 pw2f1ocnv 43886 cnvintabd 44451 clcnvlem 44471 frege133 44844 binomcxplemnotnn0 45188 fzisoeu 46141 gricushgr 48841 uspgrlim 48916 tposideq 49822