![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > keepel | Structured version Visualization version GIF version |
Description: Keep a membership hypothesis for weak deduction theorem, when special case 𝐵 ∈ 𝐶 is provable. (Contributed by NM, 14-Aug-1999.) |
Ref | Expression |
---|---|
keepel.1 | ⊢ 𝐴 ∈ 𝐶 |
keepel.2 | ⊢ 𝐵 ∈ 𝐶 |
Ref | Expression |
---|---|
keepel | ⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2718 | . 2 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝐴 ∈ 𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶)) | |
2 | eleq1 2718 | . 2 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝐵 ∈ 𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶)) | |
3 | keepel.1 | . 2 ⊢ 𝐴 ∈ 𝐶 | |
4 | keepel.2 | . 2 ⊢ 𝐵 ∈ 𝐶 | |
5 | 1, 2, 3, 4 | keephyp 4185 | 1 ⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2030 ifcif 4119 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-if 4120 |
This theorem is referenced by: ifex 4189 xaddf 12093 sadcf 15222 ramcl 15780 setcepi 16785 abvtrivd 18888 mvrf1 19473 mplcoe3 19514 psrbagsn 19543 evlslem1 19563 marep01ma 20514 dscmet 22424 dscopn 22425 i1f1lem 23501 i1f1 23502 itg2const 23552 cxpval 24455 cxpcl 24465 recxpcl 24466 sqff1o 24953 chtublem 24981 dchrmulid2 25022 bposlem1 25054 lgsval 25071 lgsfcl2 25073 lgscllem 25074 lgsval2lem 25077 lgsneg 25091 lgsdilem 25094 lgsdir2 25100 lgsdir 25102 lgsdi 25104 lgsne0 25105 dchrisum0flblem1 25242 dchrisum0flblem2 25243 dchrisum0fno1 25245 rpvmasum2 25246 omlsi 28391 sgnsf 29857 psgnfzto1stlem 29978 indfval 30206 ddemeas 30427 eulerpartlemb 30558 eulerpartlemgs2 30570 sqdivzi 31736 poimirlem16 33555 poimirlem19 33558 pw2f1ocnv 37921 flcidc 38061 arearect 38118 ifcli 39643 sqwvfourb 40764 fouriersw 40766 hspval 41144 |
Copyright terms: Public domain | W3C validator |