![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > recnprss | Structured version Visualization version GIF version |
Description: Both ℝ and ℂ are subsets of ℂ. (Contributed by Mario Carneiro, 10-Feb-2015.) |
Ref | Expression |
---|---|
recnprss | ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpri 4646 | . 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ)) | |
2 | ax-resscn 11189 | . . . 4 ⊢ ℝ ⊆ ℂ | |
3 | sseq1 4003 | . . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ)) | |
4 | 2, 3 | mpbiri 258 | . . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ) |
5 | eqimss 4036 | . . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ) | |
6 | 4, 5 | jaoi 856 | . 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ) |
7 | 1, 6 | syl 17 | 1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 846 = wceq 1534 ∈ wcel 2099 ⊆ wss 3944 {cpr 4626 ℂcc 11130 ℝcr 11131 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2698 ax-resscn 11189 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-v 3471 df-un 3949 df-in 3951 df-ss 3961 df-sn 4625 df-pr 4627 |
This theorem is referenced by: dvres3 25835 dvres3a 25836 dvcnp 25841 dvnff 25846 dvnadd 25852 dvnres 25854 cpnord 25858 cpncn 25859 cpnres 25860 dvadd 25864 dvmul 25865 dvaddf 25866 dvmulf 25867 dvcmul 25868 dvcmulf 25869 dvco 25872 dvcof 25873 dvmptid 25882 dvmptc 25883 dvmptres2 25887 dvmptcmul 25889 dvmptfsum 25900 dvcnvlem 25901 dvcnv 25902 dvlip2 25921 taylfvallem1 26284 tayl0 26289 taylply2 26295 taylply2OLD 26296 taylply 26297 dvtaylp 26298 dvntaylp 26299 taylthlem1 26301 ulmdvlem1 26329 ulmdvlem3 26331 ulmdv 26332 dvsconst 43739 dvsid 43740 dvsef 43741 dvconstbi 43743 expgrowth 43744 dvdmsscn 45296 dvnmptdivc 45298 dvnmptconst 45301 dvnxpaek 45302 dvnmul 45303 dvnprodlem3 45308 |
Copyright terms: Public domain | W3C validator |