Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-cdeq | Unicode version |
Description: Define conditional equality. All the notation to the left of the is fake; the parentheses and arrows are all part of the notation, which could equally well be written CondEq. On the right side is the actual implication arrow. The reason for this definition is to "flatten" the structure on the right side (whose tree structure is something like (wi (wceq (cv vx) (cv vy)) wph) ) into just (wcdeq vx vy wph). (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
df-cdeq | CondEq |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 | |
2 | vx | . . 3 | |
3 | vy | . . 3 | |
4 | 1, 2, 3 | wcdeq 2747 | . 2 CondEq |
5 | 2, 3 | weq 1392 | . . 3 |
6 | 5, 1 | wi 4 | . 2 |
7 | 4, 6 | wb 98 | 1 CondEq |
Colors of variables: wff set class |
This definition is referenced by: cdeqi 2749 cdeqri 2750 bdcdeq 9959 |
Copyright terms: Public domain | W3C validator |