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 5112 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑦𝐴𝑥 → 𝑦𝐵𝑥)) | |
2 | 1 | ssopab2dv 5440 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} ⊆ {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥}) |
3 | df-cnv 5565 | . 2 ⊢ ◡𝐴 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} | |
4 | df-cnv 5565 | . 2 ⊢ ◡𝐵 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥} | |
5 | 2, 3, 4 | 3sstr4g 4014 | 1 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3938 class class class wbr 5068 {copab 5130 ◡ccnv 5556 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-in 3945 df-ss 3954 df-br 5069 df-opab 5131 df-cnv 5565 |
This theorem is referenced by: cnveq 5746 rnss 5811 relcnvtrg 6121 funss 6376 funres11 6433 funcnvres 6434 foimacnv 6634 funcnvuni 7638 tposss 7895 vdwnnlem1 16333 structcnvcnv 16499 catcoppccl 17370 cnvps 17824 tsrdir 17850 ustneism 22834 metustsym 23167 metust 23170 pi1xfrcnv 23663 eulerpartlemmf 31635 relcnveq3 35580 elrelscnveq3 35733 disjss 35966 cnvssb 39953 trclubgNEW 39985 clrellem 39989 clcnvlem 39990 cnvrcl0 39992 cnvtrcl0 39993 cnvtrrel 40022 relexpaddss 40070 |
Copyright terms: Public domain | W3C validator |