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 5780 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) | |
2 | cnvss 5780 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴) | |
3 | 1, 2 | anim12i 613 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴)) |
4 | eqss 3941 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
5 | eqss 3941 | . 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴)) | |
6 | 3, 4, 5 | 3imtr4i 292 | 1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1542 ⊆ wss 3892 ◡ccnv 5589 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-ext 2711 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1545 df-ex 1787 df-sb 2072 df-clab 2718 df-cleq 2732 df-clel 2818 df-v 3433 df-in 3899 df-ss 3909 df-br 5080 df-opab 5142 df-cnv 5598 |
This theorem is referenced by: cnveqi 5782 cnveqd 5783 rneq 5844 cnveqb 6098 predeq123 6202 f1eq1 6663 f1ssf1 6745 f1o00 6748 foeqcnvco 7168 funcnvuni 7772 tposfn2 8055 ereq1 8488 cnvfi 8945 infeq3 9217 1arith 16626 vdwmc 16677 vdwnnlem1 16694 ramub2 16713 rami 16714 isps 18284 istsr 18299 isdir 18314 isrim0 19965 psrbag 21118 psrbaglefi 21133 psrbaglefiOLD 21134 iscn 22384 ishmeo 22908 symgtgp 23255 ustincl 23357 ustdiag 23358 ustinvel 23359 ustexhalf 23360 ustexsym 23365 ust0 23369 isi1f 24836 itg1val 24845 fta1lem 25465 fta1 25466 vieta1lem2 25469 vieta1 25470 sqff1o 26329 istrl 28061 isspth 28088 upgrwlkdvspth 28103 uhgrwkspthlem1 28117 0spth 28486 nlfnval 30239 padct 31050 tocyc01 31381 cycpmconjslem2 31418 indf1ofs 31990 ismbfm 32215 issibf 32296 sitgfval 32304 eulerpartlemelr 32320 eulerpartleme 32326 eulerpartlemo 32328 eulerpartlemt0 32332 eulerpartlemt 32334 eulerpartgbij 32335 eulerpartlemr 32337 eulerpartlemgs2 32343 eulerpartlemn 32344 eulerpart 32345 funen1cnv 33056 iscvm 33217 elmpst 33494 elsymrels2 36663 elsymrels4 36665 symreleq 36668 elrefsymrels2 36679 eleqvrels2 36701 eldisjs 36829 lkrval 37098 ltrncnvnid 38137 cdlemkuu 38905 pw2f1o2val 40858 pwfi2f1o 40918 clcnvlem 41201 rfovcnvf1od 41582 fsovrfovd 41587 issmflem 44231 isrngisom 45423 |
Copyright terms: Public domain | W3C validator |