| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rspcsbela | Structured version Visualization version GIF version | ||
| Description: Special case related to rspsbc 3879. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.) |
| Ref | Expression |
|---|---|
| rspcsbela | ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rspsbc 3879 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → [𝐴 / 𝑥]𝐶 ∈ 𝐷)) | |
| 2 | sbcel1g 4416 | . . 3 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 ∈ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)) | |
| 3 | 1, 2 | sylibd 239 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)) |
| 4 | 3 | imp 406 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 ∀wral 3061 [wsbc 3788 ⦋csb 3899 |
| 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 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ral 3062 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-nul 4334 |
| This theorem is referenced by: el2mpocsbcl 8110 mptnn0fsupp 14038 mptnn0fsuppr 14040 fsumzcl2 15775 fsummsnunz 15790 fsumsplitsnun 15791 modfsummodslem1 15828 fprodmodd 16033 sumeven 16424 sumodd 16425 gsummpt1n0 19983 gsummptnn0fz 20004 telgsumfzslem 20006 telgsumfzs 20007 telgsums 20011 mptscmfsupp0 20925 coe1fzgsumdlem 22307 gsummoncoe1 22312 evl1gsumdlem 22360 madugsum 22649 iunmbl2 25592 gsumvsca1 33232 gsumvsca2 33233 rmfsupp2 33242 esum2dlem 34093 esumiun 34095 evl1gprodd 42118 idomnnzgmulnz 42134 deg1gprod 42141 f1o2d2 42274 iblsplitf 45985 fsummsndifre 47359 fsumsplitsndif 47360 fsummmodsndifre 47361 fsummmodsnunz 47362 |
| Copyright terms: Public domain | W3C validator |