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 3451 ^◡ccnv 5650

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 2733 ax-sep 5249 ax-pow 5327 ax-pr 5391 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 2740 df-cleq 2753 df-clel 2836 df-ral 3078 df-rex 3088 df-rab 3414 df-v 3453 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5104 df-opab 5168 df-xp 5657 df-rel 5658 df-cnv 5659 df-dm 5661 df-rn 5662

This theorem is used by: f1oexbi 7929 funcnvuni 7933 cnvf1o 8111 brtpos2 8233 pw2f1o 9085 sbthlem10 9099 fodomr 9131 ssenen 9154 cnfcomlem 9684 infxpenlem 10073 enfin2i 10380 fin1a2lem7 10465 fpwwe 10712 canthwelem 10716 axdc4uzlem 14106 hashfacen 14579 catcisolem 18265 oduleval 18443 gicsubgen 19473 isunit 20583 znle 21822 evpmss 21872 psgnevpmb 21873 ptbasfi 23880 nghmfval 25021 fta1glem2 26467 fta1blem 26469 lgsqrlem4 27658 tocycf 33660 evpmval 33688 altgnsg 33692 elrgspnsubrunlem2 33791 elrspunidl 33960 1arithidom 34051 irngval 34299 locfinreflem 34454 zarcmplem 34495 qqhval 34586 mbfmcnt 34883 derangenlem 35905 mthmval 36309 colinearex 36795 fvline 36879 ptrest 38505 poimir 38539 tendoi2 41820 dihopelvalcpre 42273 pw2f1ocnv 43997 cnvintabd 44562 clcnvlem 44582 frege133 44955 binomcxplemnotnn0 45299 fzisoeu 46259 gricushgr 48959 uspgrlim 49034 tposideq 49940