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. (Contributed by NM, 13-Aug-1995.) |
Ref | Expression |
---|---|
cnveq | ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvss 5294 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) | |
2 | cnvss 5294 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴) | |
3 | 1, 2 | anim12i 590 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴)) |
4 | eqss 3618 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
5 | eqss 3618 | . 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴)) | |
6 | 3, 4, 5 | 3imtr4i 281 | 1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 ⊆ wss 3574 ◡ccnv 5113 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-in 3581 df-ss 3588 df-br 4654 df-opab 4713 df-cnv 5122 |
This theorem is referenced by: cnveqi 5297 cnveqd 5298 rneq 5351 cnveqb 5590 predeq123 5681 f1eq1 6096 f1ssf1 6168 f1o00 6171 foeqcnvco 6555 funcnvuni 7119 tposfn2 7374 ereq1 7749 infeq3 8386 1arith 15631 vdwmc 15682 vdwnnlem1 15699 ramub2 15718 rami 15719 isps 17202 istsr 17217 isdir 17232 isrim0 18723 psrbag 19364 psrbaglefi 19372 iscn 21039 ishmeo 21562 symgtgp 21905 ustincl 22011 ustdiag 22012 ustinvel 22013 ustexhalf 22014 ustexsym 22019 ust0 22023 isi1f 23441 itg1val 23450 fta1lem 24062 fta1 24063 vieta1lem2 24066 vieta1 24067 sqff1o 24908 istrl 26593 isspth 26620 upgrwlkdvspth 26635 uhgrwkspthlem1 26649 0spth 26987 nlfnval 28740 padct 29497 indf1ofs 30088 ismbfm 30314 issibf 30395 sitgfval 30403 eulerpartlemelr 30419 eulerpartleme 30425 eulerpartlemo 30427 eulerpartlemt0 30431 eulerpartlemt 30433 eulerpartgbij 30434 eulerpartlemr 30436 eulerpartlemgs2 30442 eulerpartlemn 30443 eulerpart 30444 iscvm 31241 elmpst 31433 lkrval 34375 ltrncnvnid 35413 cdlemkuu 36183 pw2f1o2val 37606 pwfi2f1o 37666 clcnvlem 37930 rfovcnvf1od 38298 fsovrfovd 38303 issmflem 40936 isrngisom 41896 |
Copyright terms: Public domain | W3C validator |