![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnv0 | Structured version Visualization version Unicode version |
Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.) |
Ref | Expression |
---|---|
cnv0 |
![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relcnv 5207 |
. 2
![]() ![]() ![]() ![]() | |
2 | rel0 4958 |
. 2
![]() ![]() ![]() | |
3 | vex 3048 |
. . . 4
![]() ![]() ![]() ![]() | |
4 | vex 3048 |
. . . 4
![]() ![]() ![]() ![]() | |
5 | 3, 4 | opelcnv 5016 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | noel 3735 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | noel 3735 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 6, 7 | 2false 352 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 5, 8 | bitr4i 256 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 1, 2, 9 | eqrelriiv 4929 |
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 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pr 4639 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3047 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-sn 3969 df-pr 3971 df-op 3975 df-br 4403 df-opab 4462 df-xp 4840 df-rel 4841 df-cnv 4842 |
This theorem is referenced by: xp0 5255 cnveq0 5292 co01 5350 funcnv0 5640 f10 5845 f1o00 5847 tpos0 7003 oduleval 16377 ust0 21234 nghmfval 21727 isnghm 21728 nghmfvalOLD 21745 isnghmOLD 21746 0pth 25300 1pthonlem1 25319 mthmval 30213 resnonrel 36198 cononrel1 36200 cononrel2 36201 cnvrcl0 36232 0cnf 37754 mbf0 37834 |
Copyright terms: Public domain | W3C validator |