![]() |
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 5193 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑦𝐴𝑥 → 𝑦𝐵𝑥)) | |
2 | 1 | ssopab2dv 5552 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}) |
3 | df-cnv 5685 | . 2 ⊢ ◡𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} | |
4 | df-cnv 5685 | . 2 ⊢ ◡𝐵 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥} | |
5 | 2, 3, 4 | 3sstr4g 4028 | 1 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3949 class class class wbr 5149 {copab 5211 ◡ccnv 5676 |
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 3477 df-in 3956 df-ss 3966 df-br 5150 df-opab 5212 df-cnv 5685 |
This theorem is referenced by: cnveq 5874 rnss 5939 relcnvtrg 6266 predrelss 6339 funss 6568 funres11 6626 funcnvres 6627 foimacnv 6851 funcnvuni 7922 tposss 8212 vdwnnlem1 16928 structcnvcnv 17086 catcoppccl 18067 catcoppcclOLD 18068 cnvps 18531 tsrdir 18557 ustneism 23728 metustsym 24064 metust 24067 pi1xfrcnv 24573 eulerpartlemmf 33374 relcnveq3 37190 elrelscnveq3 37361 disjss 37601 cnvssb 42337 trclubgNEW 42369 clrellem 42373 clcnvlem 42374 cnvrcl0 42376 cnvtrcl0 42377 cnvtrrel 42421 relexpaddss 42469 |
Copyright terms: Public domain | W3C validator |