Definition df-cdeq 2973

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.)

Assertion

Ref	Expression
df-cdeq	⊢ (CondEq(𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑦 → 𝜑))

Detailed syntax breakdown of Definition df-cdeq

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4	1, 2, 3	wcdeq 2972	. 2 wff CondEq(𝑥 = 𝑦 → 𝜑)
5	2, 3	weq 1517	. . 3 wff 𝑥 = 𝑦
6	5, 1	wi 4	. 2 wff (𝑥 = 𝑦 → 𝜑)
7	4, 6	wb 105	1 wff (CondEq(𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑦 → 𝜑))

This definition is referenced by:  cdeqi  2974  cdeqri  2975  bdcdeq  15485