![]() |
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 5150 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑦𝐴𝑥 → 𝑦𝐵𝑥)) | |
2 | 1 | ssopab2dv 5509 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}) |
3 | df-cnv 5642 | . 2 ⊢ ◡𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} | |
4 | df-cnv 5642 | . 2 ⊢ ◡𝐵 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥} | |
5 | 2, 3, 4 | 3sstr4g 3990 | 1 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3911 class class class wbr 5106 {copab 5168 ◡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: cnveq 5830 rnss 5895 relcnvtrg 6219 predrelss 6292 funss 6521 funres11 6579 funcnvres 6580 foimacnv 6802 funcnvuni 7869 tposss 8159 vdwnnlem1 16872 structcnvcnv 17030 catcoppccl 18008 catcoppcclOLD 18009 cnvps 18472 tsrdir 18498 ustneism 23591 metustsym 23927 metust 23930 pi1xfrcnv 24436 eulerpartlemmf 33032 relcnveq3 36828 elrelscnveq3 36999 disjss 37239 cnvssb 41946 trclubgNEW 41978 clrellem 41982 clcnvlem 41983 cnvrcl0 41985 cnvtrcl0 41986 cnvtrrel 42030 relexpaddss 42078 |
Copyright terms: Public domain | W3C validator |