Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > iffalse | GIF version |
Description: Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.) |
Ref | Expression |
---|---|
iffalse | ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-if 3526 | . 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} | |
2 | dedlemb 965 | . . 3 ⊢ (¬ 𝜑 → (𝑥 ∈ 𝐵 ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑)))) | |
3 | 2 | abbi2dv 2289 | . 2 ⊢ (¬ 𝜑 → 𝐵 = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}) |
4 | 1, 3 | eqtr4id 2222 | 1 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ∨ wo 703 = wceq 1348 ∈ wcel 2141 {cab 2156 ifcif 3525 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-11 1499 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-if 3526 |
This theorem is referenced by: iffalsei 3534 iffalsed 3535 ifnefalse 3536 ifsbdc 3537 ifcldadc 3554 ifeq1dadc 3555 ifbothdadc 3556 ifbothdc 3557 ifiddc 3558 ifcldcd 3560 ifnotdc 3561 ifandc 3562 fidifsnen 6844 nnnninf 7098 uzin 9506 modifeq2int 10329 bcval 10670 bcval3 10672 sumrbdclem 11327 fsum3cvg 11328 summodclem2a 11331 sumsplitdc 11382 prodrbdclem 11521 fproddccvg 11522 prodssdc 11539 flodddiv4 11880 gcdn0val 11903 dfgcd2 11956 lcmn0val 12007 pcgcd 12269 pcmptcl 12281 pcmpt 12282 pcmpt2 12283 pcprod 12285 fldivp1 12287 unct 12384 lgsneg 13678 lgsdilem 13681 lgsdir2 13687 lgsdir 13689 lgsdi 13691 lgsne0 13692 |
Copyright terms: Public domain | W3C validator |