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 5113 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑦𝐴𝑥 → 𝑦𝐵𝑥)) | |
2 | 1 | ssopab2dv 5441 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} ⊆ {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥}) |
3 | df-cnv 5566 | . 2 ⊢ ◡𝐴 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} | |
4 | df-cnv 5566 | . 2 ⊢ ◡𝐵 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥} | |
5 | 2, 3, 4 | 3sstr4g 4015 | 1 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3939 class class class wbr 5069 {copab 5131 ◡ccnv 5557 |
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 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-in 3946 df-ss 3955 df-br 5070 df-opab 5132 df-cnv 5566 |
This theorem is referenced by: cnveq 5747 rnss 5812 relcnvtrg 6122 funss 6377 funres11 6434 funcnvres 6435 foimacnv 6635 funcnvuni 7639 tposss 7896 vdwnnlem1 16334 structcnvcnv 16500 catcoppccl 17371 cnvps 17825 tsrdir 17851 ustneism 22835 metustsym 23168 metust 23171 pi1xfrcnv 23664 eulerpartlemmf 31637 relcnveq3 35582 elrelscnveq3 35735 disjss 35968 cnvssb 39952 trclubgNEW 39984 clrellem 39988 clcnvlem 39989 cnvrcl0 39991 cnvtrcl0 39992 cnvtrrel 40021 relexpaddss 40069 |
Copyright terms: Public domain | W3C validator |