![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnvexg | Structured version Visualization version Unicode version |
Description: The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 17-Mar-1998.) |
Ref | Expression |
---|---|
cnvexg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relcnv 5185 |
. . 3
![]() ![]() ![]() ![]() | |
2 | relssdmrn 5335 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | df-rn 4823 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | rnexg 6713 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | syl5eqelr 2535 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | dfdm4 5005 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | dmexg 6712 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 7, 8 | syl5eqelr 2535 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | xpexg 6581 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 6, 9, 10 | syl2anc 671 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | ssexg 4521 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | 3, 11, 12 | sylancr 674 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-8 1893 ax-9 1900 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 ax-sep 4497 ax-nul 4506 ax-pow 4554 ax-pr 4612 ax-un 6571 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 988 df-tru 1451 df-ex 1668 df-nf 1672 df-sb 1802 df-eu 2304 df-mo 2305 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-ne 2624 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3015 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-nul 3700 df-if 3850 df-pw 3921 df-sn 3937 df-pr 3939 df-op 3943 df-uni 4169 df-br 4375 df-opab 4434 df-xp 4818 df-rel 4819 df-cnv 4820 df-dm 4822 df-rn 4823 |
This theorem is referenced by: cnvex 6728 relcnvexb 6729 cofunex2g 6746 tposexg 6974 cnven 7632 fopwdom 7667 domssex2 7719 domssex 7720 cnvfi 7843 mapfienlem2 7906 wemapwe 8189 fin1a2lem7 8823 fpwwe 9058 hasheqf1oi 12528 brtrclfvcnv 13079 brcnvtrclfvcnv 13080 relexpcnv 13109 relexpnnrn 13119 relexpaddg 13127 imasle 15435 cnvps 16469 gsumvalx 16524 symginv 17054 tposmap 19493 metustel 21576 metustss 21577 metustfbas 21583 metuel2 21591 psmetutop 21593 restmetu 21596 itg2gt0 22730 nlfnval 27546 cnvct 28307 ffsrn 28322 eulerpartlemgs2 29219 orvcval 29296 coinfliprv 29321 lkrval 32656 pw2f1o2val 35896 lmhmlnmsplit 35947 cnvcnvintabd 36208 clrellem 36231 relexpaddss 36312 cnvtrclfv 36318 rntrclfvRP 36325 xpexb 36808 sge0f1o 38283 |
Copyright terms: Public domain | W3C validator |