Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ifcli | Structured version Visualization version GIF version |
Description: Inference associated with ifcl 4507. Membership (closure) of a conditional operator. Also usable to keep a membership hypothesis for the weak deduction theorem dedth 4519 when the special case 𝐵 ∈ 𝐶 is provable. (Contributed by NM, 14-Aug-1999.) (Proof shortened by BJ, 1-Sep-2022.) |
Ref | Expression |
---|---|
ifcli.1 | ⊢ 𝐴 ∈ 𝐶 |
ifcli.2 | ⊢ 𝐵 ∈ 𝐶 |
Ref | Expression |
---|---|
ifcli | ⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifcli.1 | . 2 ⊢ 𝐴 ∈ 𝐶 | |
2 | ifcli.2 | . 2 ⊢ 𝐵 ∈ 𝐶 | |
3 | ifcl 4507 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶) | |
4 | 1, 2, 3 | mp2an 688 | 1 ⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 ifcif 4463 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-if 4464 |
This theorem is referenced by: ifex 4511 xaddf 12605 sadcf 15790 ramcl 16353 setcepi 17336 abvtrivd 19540 mvrf1 20133 mplcoe3 20175 psrbagsn 20203 evlslem1 20223 marep01ma 21197 dscmet 23109 dscopn 23110 i1f1lem 24217 i1f1 24218 itg2const 24268 cxpval 25174 cxpcl 25184 recxpcl 25185 sqff1o 25686 chtublem 25714 dchrmulid2 25755 bposlem1 25787 lgsval 25804 lgsfcl2 25806 lgscllem 25807 lgsval2lem 25810 lgsneg 25824 lgsdilem 25827 lgsdir2 25833 lgsdir 25835 lgsdi 25837 lgsne0 25838 dchrisum0flblem1 26011 dchrisum0flblem2 26012 dchrisum0fno1 26014 rpvmasum2 26015 omlsi 29108 psgnfzto1stlem 30669 sgnsf 30731 indfval 31174 ddemeas 31394 eulerpartlemb 31525 eulerpartlemgs2 31537 ex-sategoelel12 32571 sqdivzi 32856 poimirlem16 34789 poimirlem19 34792 pw2f1ocnv 39512 flcidc 39652 arearect 39700 limsup10exlem 41929 sqwvfourb 42391 fouriersw 42393 hspval 42768 |
Copyright terms: Public domain | W3C validator |