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 3782. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.) |
Ref | Expression |
---|---|
rspcsbela | ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspsbc 3782 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → [𝐴 / 𝑥]𝐶 ∈ 𝐷)) | |
2 | sbcel1g 4318 | . . 3 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 ∈ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)) | |
3 | 1, 2 | sylibd 242 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)) |
4 | 3 | imp 410 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2110 ∀wral 3054 [wsbc 3687 ⦋csb 3802 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ral 3059 df-v 3403 df-sbc 3688 df-csb 3803 df-dif 3860 df-nul 4228 |
This theorem is referenced by: el2mpocsbcl 7842 mptnn0fsupp 13553 mptnn0fsuppr 13555 fsumzcl2 15285 fsummsnunz 15299 fsumsplitsnun 15300 modfsummodslem1 15337 fprodmodd 15540 sumeven 15929 sumodd 15930 gsummpt1n0 19322 gsummptnn0fz 19343 telgsumfzslem 19345 telgsumfzs 19346 telgsums 19350 mptscmfsupp0 19936 coe1fzgsumdlem 21194 gsummoncoe1 21197 evl1gsumdlem 21244 madugsum 21512 iunmbl2 24426 gsumvsca1 31170 gsumvsca2 31171 rmfsupp2 31183 esum2dlem 31744 esumiun 31746 iblsplitf 43140 fsummsndifre 44451 fsumsplitsndif 44452 fsummmodsndifre 44453 fsummmodsnunz 44454 |
Copyright terms: Public domain | W3C validator |