![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnveq | Structured version Visualization version GIF version |
Description: Equality theorem for converse relation. (Contributed by NM, 13-Aug-1995.) |
Ref | Expression |
---|---|
cnveq | ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvss 5542 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) | |
2 | cnvss 5542 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴) | |
3 | 1, 2 | anim12i 606 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴)) |
4 | eqss 3836 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
5 | eqss 3836 | . 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴)) | |
6 | 3, 4, 5 | 3imtr4i 284 | 1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 = wceq 1601 ⊆ wss 3792 ◡ccnv 5356 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-in 3799 df-ss 3806 df-br 4889 df-opab 4951 df-cnv 5365 |
This theorem is referenced by: cnveqi 5544 cnveqd 5545 rneq 5598 cnveqb 5845 predeq123 5936 f1eq1 6348 f1ssf1 6424 f1o00 6427 foeqcnvco 6829 funcnvuni 7400 tposfn2 7658 ereq1 8035 infeq3 8676 1arith 16039 vdwmc 16090 vdwnnlem1 16107 ramub2 16126 rami 16127 isps 17592 istsr 17607 isdir 17622 isrim0 19116 psrbag 19765 psrbaglefi 19773 iscn 21451 ishmeo 21975 symgtgp 22317 ustincl 22423 ustdiag 22424 ustinvel 22425 ustexhalf 22426 ustexsym 22431 ust0 22435 isi1f 23882 itg1val 23891 fta1lem 24503 fta1 24504 vieta1lem2 24507 vieta1 24508 sqff1o 25364 istrl 27051 isspth 27080 upgrwlkdvspth 27095 uhgrwkspthlem1 27109 0spth 27533 nlfnval 29316 padct 30067 indf1ofs 30690 ismbfm 30916 issibf 30997 sitgfval 31005 eulerpartlemelr 31021 eulerpartleme 31027 eulerpartlemo 31029 eulerpartlemt0 31033 eulerpartlemt 31035 eulerpartgbij 31036 eulerpartlemr 31038 eulerpartlemgs2 31044 eulerpartlemn 31045 eulerpart 31046 iscvm 31844 elmpst 32036 elsymrels2 34932 elsymrels4 34934 symreleq 34937 elrefsymrels2 34948 eleqvrels2 34969 lkrval 35247 ltrncnvnid 36286 cdlemkuu 37054 pw2f1o2val 38575 pwfi2f1o 38635 clcnvlem 38897 rfovcnvf1od 39264 fsovrfovd 39269 issmflem 41873 isrngisom 42921 |
Copyright terms: Public domain | W3C validator |