| 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 5187 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑦𝐴𝑥 → 𝑦𝐵𝑥)) | |
| 2 | 1 | ssopab2dv 5556 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} ⊆ {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥}) |
| 3 | df-cnv 5693 | . 2 ⊢ ◡𝐴 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} | |
| 4 | df-cnv 5693 | . 2 ⊢ ◡𝐵 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥} | |
| 5 | 2, 3, 4 | 3sstr4g 4037 | 1 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ⊆ wss 3951 class class class wbr 5143 {copab 5205 ◡ccnv 5684 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ss 3968 df-br 5144 df-opab 5206 df-cnv 5693 |
| This theorem is referenced by: cnveq 5884 rnss 5950 relcnvtrg 6286 predrelss 6358 funss 6585 funres11 6643 funcnvres 6644 foimacnv 6865 funcnvuni 7954 tposss 8252 vdwnnlem1 17033 structcnvcnv 17190 catcoppccl 18162 cnvps 18623 tsrdir 18649 ustneism 24232 metustsym 24568 metust 24571 pi1xfrcnv 25090 eulerpartlemmf 34377 relcnveq3 38322 elrelscnveq3 38492 disjss 38732 cnvssb 43599 trclubgNEW 43631 clrellem 43635 clcnvlem 43636 cnvrcl0 43638 cnvtrcl0 43639 cnvtrrel 43683 relexpaddss 43731 |
| Copyright terms: Public domain | W3C validator |