![]() |
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 4535. Membership (closure) of a conditional operator. Also usable to keep a membership hypothesis for the weak deduction theorem dedth 4548 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 4535 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶) | |
4 | 1, 2, 3 | mp2an 691 | 1 ⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 ifcif 4490 |
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-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-if 4491 |
This theorem is referenced by: ifex 4540 xaddf 13152 sadcf 16341 ramcl 16909 setcepi 17982 abvtrivd 20342 mvrf1 21417 mplcoe3 21462 psrbagsn 21494 evlslem1 21515 marep01ma 22032 dscmet 23951 dscopn 23952 i1f1lem 25076 i1f1 25077 itg2const 25128 cxpval 26042 cxpcl 26052 recxpcl 26053 sqff1o 26554 chtublem 26582 dchrmullid 26623 bposlem1 26655 lgsval 26672 lgsfcl2 26674 lgscllem 26675 lgsval2lem 26678 lgsneg 26692 lgsdilem 26695 lgsdir2 26701 lgsdir 26703 lgsdi 26705 lgsne0 26706 dchrisum0flblem1 26879 dchrisum0flblem2 26880 dchrisum0fno1 26882 rpvmasum2 26883 omlsi 30395 psgnfzto1stlem 32005 sgnsf 32067 indfval 32679 ddemeas 32899 eulerpartlemb 33032 eulerpartlemgs2 33044 ex-sategoelel12 34085 sqdivzi 34363 poimirlem16 36144 poimirlem19 36147 pw2f1ocnv 41408 flcidc 41548 arearect 41596 sqrtcval 42005 sqrtcval2 42006 resqrtval 42007 imsqrtval 42008 limsup10exlem 44103 sqwvfourb 44560 fouriersw 44562 hspval 44940 |
Copyright terms: Public domain | W3C validator |