Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cdeq Structured version   Unicode version

Definition df-cdeq 3145
 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
StepHypRef Expression
1 wph . . 3
2 vx . . 3
3 vy . . 3
41, 2, 3wcdeq 3144 . 2 CondEq
52, 3weq 1653 . . 3
65, 1wi 4 . 2
74, 6wb 177 1 CondEq
 Colors of variables: wff set class This definition is referenced by:  cdeqi  3146  cdeqri  3147
 Copyright terms: Public domain W3C validator