![]() |
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 3836. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.) |
Ref | Expression |
---|---|
rspcsbela | ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspsbc 3836 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → [𝐴 / 𝑥]𝐶 ∈ 𝐷)) | |
2 | sbcel1g 4374 | . . 3 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 ∈ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)) | |
3 | 1, 2 | sylibd 238 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)) |
4 | 3 | imp 408 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 ∀wral 3061 [wsbc 3740 ⦋csb 3856 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3062 df-v 3446 df-sbc 3741 df-csb 3857 df-dif 3914 df-nul 4284 |
This theorem is referenced by: el2mpocsbcl 8018 mptnn0fsupp 13908 mptnn0fsuppr 13910 fsumzcl2 15629 fsummsnunz 15644 fsumsplitsnun 15645 modfsummodslem1 15682 fprodmodd 15885 sumeven 16274 sumodd 16275 gsummpt1n0 19747 gsummptnn0fz 19768 telgsumfzslem 19770 telgsumfzs 19771 telgsums 19775 mptscmfsupp0 20402 coe1fzgsumdlem 21688 gsummoncoe1 21691 evl1gsumdlem 21738 madugsum 22008 iunmbl2 24937 gsumvsca1 32110 gsumvsca2 32111 rmfsupp2 32122 esum2dlem 32748 esumiun 32750 iblsplitf 44297 fsummsndifre 45650 fsumsplitsndif 45651 fsummmodsndifre 45652 fsummmodsnunz 45653 |
Copyright terms: Public domain | W3C validator |