![]() |
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 4420 | . 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ)) | |
2 | ax-resscn 10329 | . . . 4 ⊢ ℝ ⊆ ℂ | |
3 | sseq1 3845 | . . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ)) | |
4 | 2, 3 | mpbiri 250 | . . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ) |
5 | eqimss 3876 | . . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ) | |
6 | 4, 5 | jaoi 846 | . 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ) |
7 | 1, 6 | syl 17 | 1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 836 = wceq 1601 ∈ wcel 2107 ⊆ wss 3792 {cpr 4400 ℂcc 10270 ℝcr 10271 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 ax-resscn 10329 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-v 3400 df-un 3797 df-in 3799 df-ss 3806 df-sn 4399 df-pr 4401 |
This theorem is referenced by: dvres3 24114 dvres3a 24115 dvcnp 24119 dvnff 24123 dvnadd 24129 dvnres 24131 cpnord 24135 cpncn 24136 cpnres 24137 dvadd 24140 dvmul 24141 dvaddf 24142 dvmulf 24143 dvcmul 24144 dvcmulf 24145 dvco 24147 dvcof 24148 dvmptid 24157 dvmptc 24158 dvmptres2 24162 dvmptcmul 24164 dvmptfsum 24175 dvcnvlem 24176 dvcnv 24177 dvlip2 24195 taylfvallem1 24548 tayl0 24553 taylply2 24559 taylply 24560 dvtaylp 24561 dvntaylp 24562 taylthlem1 24564 ulmdvlem1 24591 ulmdvlem3 24593 ulmdv 24594 dvsconst 39485 dvsid 39486 dvsef 39487 dvconstbi 39489 expgrowth 39490 dvdmsscn 41079 dvnmptdivc 41081 dvnmptconst 41084 dvnxpaek 41085 dvnmul 41086 dvnprodlem3 41091 |
Copyright terms: Public domain | W3C validator |