![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnvex | Structured version Visualization version GIF version |
Description: The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 19-Dec-2003.) |
Ref | Expression |
---|---|
cnvex.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
cnvex | ⊢ ◡𝐴 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvex.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | cnvexg 7442 | . 2 ⊢ (𝐴 ∈ V → ◡𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ◡𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2051 Vcvv 3408 ◡ccnv 5402 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2743 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-ral 3086 df-rex 3087 df-rab 3090 df-v 3410 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-br 4926 df-opab 4988 df-xp 5409 df-rel 5410 df-cnv 5411 df-dm 5413 df-rn 5414 |
This theorem is referenced by: f1oexbi 7446 funcnvuni 7449 cnvf1o 7612 brtpos2 7699 pw2f1o 8416 sbthlem10 8430 fodomr 8462 ssenen 8485 cnfcomlem 8954 infxpenlem 9231 enfin2i 9539 fin1a2lem7 9624 fpwwe 9864 canthwelem 9868 axdc4uzlem 13164 hashfacen 13623 xpscfcda 16699 xpsfvalcda 16703 xpssca 16719 xpsvsca 16720 catcisolem 17236 oduleval 17611 gicsubgen 18201 isunit 19142 znle 20400 evpmss 20447 psgnevpmb 20448 ptbasfi 21908 nghmfval 23049 fta1glem2 24478 fta1blem 24480 lgsqrlem4 25642 tocycf 30479 altgnsg 30494 locfinreflem 30780 qqhval 30891 mbfmcnt 31203 derangenlem 32040 mthmval 32379 colinearex 33079 fvline 33163 ptrest 34369 poimir 34403 tendoi2 37413 dihopelvalcpre 37866 pw2f1ocnv 39068 cnvintabd 39363 clcnvlem 39384 frege133 39743 binomcxplemnotnn0 40142 fzisoeu 41028 isomushgr 43391 isomgrsym 43401 |
Copyright terms: Public domain | W3C validator |