![]() |
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 5875 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) | |
2 | cnvss 5875 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴) | |
3 | 1, 2 | anim12i 611 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴)) |
4 | eqss 3992 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
5 | eqss 3992 | . 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴)) | |
6 | 3, 4, 5 | 3imtr4i 291 | 1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 ⊆ wss 3944 ◡ccnv 5677 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ss 3961 df-br 5150 df-opab 5212 df-cnv 5686 |
This theorem is referenced by: cnveqi 5877 cnveqd 5878 rneq 5938 cnveqb 6202 predeq123 6308 f1eq1 6788 f1ssf1 6870 f1o00 6873 foeqcnvco 7309 funcnvuni 7940 tposfn2 8254 ereq1 8732 cnvfi 9205 infeq3 9505 1arith 16899 vdwmc 16950 vdwnnlem1 16967 ramub2 16986 rami 16987 isps 18563 istsr 18578 isdir 18593 isrngim 20396 isrim0OLD 20432 isrim0 20434 psrbag 21867 psrbaglefi 21882 psrbaglefiOLD 21883 iscn 23183 ishmeo 23707 symgtgp 24054 ustincl 24156 ustdiag 24157 ustinvel 24158 ustexhalf 24159 ustexsym 24164 ust0 24168 isi1f 25647 itg1val 25656 fta1lem 26287 fta1 26288 vieta1lem2 26291 vieta1 26292 sqff1o 27159 istrl 29582 isspth 29610 upgrwlkdvspth 29625 uhgrwkspthlem1 29639 0spth 30008 nlfnval 31763 padct 32583 tocyc01 32931 cycpmconjslem2 32968 indf1ofs 33776 ismbfm 34001 issibf 34084 sitgfval 34092 eulerpartlemelr 34108 eulerpartleme 34114 eulerpartlemo 34116 eulerpartlemt0 34120 eulerpartlemt 34122 eulerpartgbij 34123 eulerpartlemr 34125 eulerpartlemgs2 34131 eulerpartlemn 34132 eulerpart 34133 funen1cnv 34842 iscvm 35000 elmpst 35277 elsymrels2 38155 elsymrels4 38157 symreleq 38160 elrefsymrels2 38171 eleqvrels2 38194 eldisjs 38324 lkrval 38690 ltrncnvnid 39730 cdlemkuu 40498 pw2f1o2val 42602 pwfi2f1o 42662 clcnvlem 43195 rfovcnvf1od 43576 fsovrfovd 43581 issmflem 46253 |
Copyright terms: Public domain | W3C validator |