![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > opelcnv | Structured version Unicode version |
Description: Ordered-pair membership in converse. (Contributed by NM, 13-Aug-1995.) |
Ref | Expression |
---|---|
opelcnv.1 |
![]() ![]() ![]() ![]() |
opelcnv.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
opelcnv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelcnv.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | opelcnv.2 |
. 2
![]() ![]() ![]() ![]() | |
3 | opelcnvg 5120 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | mp2an 672 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4514 ax-nul 4522 ax-pr 4632 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-rab 2804 df-v 3073 df-dif 3432 df-un 3434 df-in 3436 df-ss 3443 df-nul 3739 df-if 3893 df-sn 3979 df-pr 3981 df-op 3985 df-br 4394 df-opab 4452 df-cnv 4949 |
This theorem is referenced by: cnvopab 5339 cnv0 5341 cnvdif 5344 dfrel2 5389 cnvcnvsn 5417 cnvresima 5428 dfco2 5438 cnviin 5475 fcnvres 5689 cnvf1olem 6773 cnvimadfsn 6802 dmtpos 6860 dftpos4 6867 tpostpos 6868 brsdom2 7538 fsumcom2 13352 gsumcom2 16581 metustsymOLD 20261 metustsym 20262 fprodcom2 27632 cnvco1 27707 cnvco2 27708 |
Copyright terms: Public domain | W3C validator |