![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnvss | Structured version Visualization version GIF version |
Description: Subset theorem for converse. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Kyle Wyonch, 27-Apr-2021.) |
Ref | Expression |
---|---|
cnvss | ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssbr 4729 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑦𝐴𝑥 → 𝑦𝐵𝑥)) | |
2 | 1 | ssopab2dv 5033 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} ⊆ {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥}) |
3 | df-cnv 5151 | . 2 ⊢ ◡𝐴 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} | |
4 | df-cnv 5151 | . 2 ⊢ ◡𝐵 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥} | |
5 | 2, 3, 4 | 3sstr4g 3679 | 1 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3607 class class class wbr 4685 {copab 4745 ◡ccnv 5142 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-in 3614 df-ss 3621 df-br 4686 df-opab 4746 df-cnv 5151 |
This theorem is referenced by: cnveq 5328 rnss 5386 relcnvtr 5693 funss 5945 funres11 6004 funcnvres 6005 foimacnv 6192 funcnvuni 7161 tposss 7398 vdwnnlem1 15746 structcnvcnv 15918 catcoppccl 16805 cnvps 17259 tsrdir 17285 ustneism 22074 metustsym 22407 metust 22410 pi1xfrcnv 22903 eulerpartlemmf 30565 relcnveq3 34233 elrelscnveq3 34381 cnvssb 38209 trclubgNEW 38242 clrellem 38246 clcnvlem 38247 cnvrcl0 38249 cnvtrcl0 38250 cnvtrrel 38279 relexpaddss 38327 |
Copyright terms: Public domain | W3C validator |