![]() |
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 4388. Membership (closure) of a conditional operator. Also usable to keep a membership hypothesis for the weak deduction theorem dedth 4400 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 4388 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶) | |
4 | 1, 2, 3 | mp2an 679 | 1 ⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2050 ifcif 4344 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-ext 2744 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-ex 1743 df-sb 2016 df-clab 2753 df-cleq 2765 df-clel 2840 df-if 4345 |
This theorem is referenced by: ifex 4392 xaddf 12432 sadcf 15660 ramcl 16219 setcepi 17218 abvtrivd 19345 mvrf1 19931 mplcoe3 19972 psrbagsn 20000 evlslem1 20020 marep01ma 20985 dscmet 22897 dscopn 22898 i1f1lem 24005 i1f1 24006 itg2const 24056 cxpval 24960 cxpcl 24970 recxpcl 24971 sqff1o 25473 chtublem 25501 dchrmulid2 25542 bposlem1 25574 lgsval 25591 lgsfcl2 25593 lgscllem 25594 lgsval2lem 25597 lgsneg 25611 lgsdilem 25614 lgsdir2 25620 lgsdir 25622 lgsdi 25624 lgsne0 25625 dchrisum0flblem1 25798 dchrisum0flblem2 25799 dchrisum0fno1 25801 rpvmasum2 25802 omlsi 28974 sgnsf 30499 psgnfzto1stlem 30720 indfval 30948 ddemeas 31169 eulerpartlemb 31300 eulerpartlemgs2 31312 sqdivzi 32508 poimirlem16 34378 poimirlem19 34381 pw2f1ocnv 39059 flcidc 39199 arearect 39247 limsup10exlem 41509 sqwvfourb 41970 fouriersw 41972 hspval 42347 |
Copyright terms: Public domain | W3C validator |