![]() |
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 5829 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) | |
2 | cnvss 5829 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴) | |
3 | 1, 2 | anim12i 614 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴)) |
4 | eqss 3960 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
5 | eqss 3960 | . 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴)) | |
6 | 3, 4, 5 | 3imtr4i 292 | 1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ⊆ wss 3911 ◡ccnv 5633 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3446 df-in 3918 df-ss 3928 df-br 5107 df-opab 5169 df-cnv 5642 |
This theorem is referenced by: cnveqi 5831 cnveqd 5832 rneq 5892 cnveqb 6149 predeq123 6255 f1eq1 6734 f1ssf1 6817 f1o00 6820 foeqcnvco 7247 funcnvuni 7869 tposfn2 8180 ereq1 8658 cnvfi 9127 infeq3 9421 1arith 16804 vdwmc 16855 vdwnnlem1 16872 ramub2 16891 rami 16892 isps 18462 istsr 18477 isdir 18492 isrim0OLD 20161 isrim0 20163 psrbag 21335 psrbaglefi 21350 psrbaglefiOLD 21351 iscn 22602 ishmeo 23126 symgtgp 23473 ustincl 23575 ustdiag 23576 ustinvel 23577 ustexhalf 23578 ustexsym 23583 ust0 23587 isi1f 25054 itg1val 25063 fta1lem 25683 fta1 25684 vieta1lem2 25687 vieta1 25688 sqff1o 26547 istrl 28686 isspth 28714 upgrwlkdvspth 28729 uhgrwkspthlem1 28743 0spth 29112 nlfnval 30865 padct 31683 tocyc01 32016 cycpmconjslem2 32053 indf1ofs 32682 ismbfm 32907 issibf 32990 sitgfval 32998 eulerpartlemelr 33014 eulerpartleme 33020 eulerpartlemo 33022 eulerpartlemt0 33026 eulerpartlemt 33028 eulerpartgbij 33029 eulerpartlemr 33031 eulerpartlemgs2 33037 eulerpartlemn 33038 eulerpart 33039 funen1cnv 33749 iscvm 33910 elmpst 34187 elsymrels2 37061 elsymrels4 37063 symreleq 37066 elrefsymrels2 37077 eleqvrels2 37100 eldisjs 37230 lkrval 37596 ltrncnvnid 38636 cdlemkuu 39404 pw2f1o2val 41406 pwfi2f1o 41466 clcnvlem 41983 rfovcnvf1od 42364 fsovrfovd 42369 issmflem 45054 isrngisom 46280 |
Copyright terms: Public domain | W3C validator |