Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-cdeq | Structured version Visualization version GIF 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 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | 1, 2, 3 | wcdeq 3702 | . 2 wff CondEq(𝑥 = 𝑦 → 𝜑) |
5 | 2, 3 | weq 1964 | . . 3 wff 𝑥 = 𝑦 |
6 | 5, 1 | wi 4 | . 2 wff (𝑥 = 𝑦 → 𝜑) |
7 | 4, 6 | wb 209 | 1 wff (CondEq(𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑦 → 𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: cdeqi 3704 cdeqri 3705 |
Copyright terms: Public domain | W3C validator |