![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rnssi | Structured version Visualization version GIF version |
Description: Subclass inference for range. (Contributed by Peter Mazsa, 24-Sep-2022.) |
Ref | Expression |
---|---|
rnssi.1 | ⊢ 𝐴 ⊆ 𝐵 |
Ref | Expression |
---|---|
rnssi | ⊢ ran 𝐴 ⊆ ran 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rnssi.1 | . 2 ⊢ 𝐴 ⊆ 𝐵 | |
2 | rnss 5657 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ran 𝐴 ⊆ ran 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3831 ran crn 5412 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-ext 2752 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2761 df-cleq 2773 df-clel 2848 df-nfc 2920 df-rab 3099 df-v 3419 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4182 df-if 4354 df-sn 4445 df-pr 4447 df-op 4451 df-br 4935 df-opab 4997 df-cnv 5419 df-dm 5421 df-rn 5422 |
This theorem is referenced by: ssrnres 5880 fssres 6378 smores 7799 brdom4 9756 smobeth 9812 nqerf 10156 catcoppccl 17238 lern 17705 gsumzres 18795 gsumzaddlem 18806 gsumzadd 18807 dprdfadd 18904 txkgen 21979 dvlog 24950 perpln2 26214 fixssrn 32929 rnresss 40900 |
Copyright terms: Public domain | W3C validator |