![]() |
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 4529. Membership (closure) of a conditional operator. Also usable to keep a membership hypothesis for the weak deduction theorem dedth 4542 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 4529 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶) | |
4 | 1, 2, 3 | mp2an 690 | 1 ⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 ifcif 4484 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-if 4485 |
This theorem is referenced by: ifex 4534 xaddf 13135 sadcf 16325 ramcl 16893 setcepi 17966 abvtrivd 20284 mvrf1 21378 mplcoe3 21423 psrbagsn 21455 evlslem1 21476 marep01ma 21993 dscmet 23912 dscopn 23913 i1f1lem 25037 i1f1 25038 itg2const 25089 cxpval 26003 cxpcl 26013 recxpcl 26014 sqff1o 26515 chtublem 26543 dchrmulid2 26584 bposlem1 26616 lgsval 26633 lgsfcl2 26635 lgscllem 26636 lgsval2lem 26639 lgsneg 26653 lgsdilem 26656 lgsdir2 26662 lgsdir 26664 lgsdi 26666 lgsne0 26667 dchrisum0flblem1 26840 dchrisum0flblem2 26841 dchrisum0fno1 26843 rpvmasum2 26844 omlsi 30232 psgnfzto1stlem 31832 sgnsf 31894 indfval 32484 ddemeas 32704 eulerpartlemb 32837 eulerpartlemgs2 32849 ex-sategoelel12 33890 sqdivzi 34170 poimirlem16 36061 poimirlem19 36064 pw2f1ocnv 41299 flcidc 41439 arearect 41487 sqrtcval 41855 sqrtcval2 41856 resqrtval 41857 imsqrtval 41858 limsup10exlem 43945 sqwvfourb 44402 fouriersw 44404 hspval 44782 |
Copyright terms: Public domain | W3C validator |