![]() |
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 5192 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑦𝐴𝑥 → 𝑦𝐵𝑥)) | |
2 | 1 | ssopab2dv 5551 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} ⊆ {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥}) |
3 | df-cnv 5684 | . 2 ⊢ ◡𝐴 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} | |
4 | df-cnv 5684 | . 2 ⊢ ◡𝐵 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥} | |
5 | 2, 3, 4 | 3sstr4g 4027 | 1 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3948 class class class wbr 5148 {copab 5210 ◡ccnv 5675 |
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 3955 df-ss 3965 df-br 5149 df-opab 5211 df-cnv 5684 |
This theorem is referenced by: cnveq 5872 rnss 5937 relcnvtrg 6263 predrelss 6336 funss 6565 funres11 6623 funcnvres 6624 foimacnv 6848 funcnvuni 7919 tposss 8209 vdwnnlem1 16925 structcnvcnv 17083 catcoppccl 18064 catcoppcclOLD 18065 cnvps 18528 tsrdir 18554 ustneism 23720 metustsym 24056 metust 24059 pi1xfrcnv 24565 eulerpartlemmf 33363 relcnveq3 37179 elrelscnveq3 37350 disjss 37590 cnvssb 42323 trclubgNEW 42355 clrellem 42359 clcnvlem 42360 cnvrcl0 42362 cnvtrcl0 42363 cnvtrrel 42407 relexpaddss 42455 |
Copyright terms: Public domain | W3C validator |